|
|
|---|
|
|
|
|---|
Tree operations specialized to *all-uri-grammar-rules*.
Function:
(defun uri-cst-matchp$ (tree elem) (declare (xargs :guard (and (treep tree) (elementp elem)))) (let ((__function__ 'uri-cst-matchp$)) (declare (ignorable __function__)) (and (tree-terminatedp tree) (tree-match-element-p tree elem *all-uri-grammar-rules*))))
Theorem:
(defthm booleanp-of-uri-cst-matchp$ (b* ((yes/no (uri-cst-matchp$ tree elem))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-matchp$-of-tree-fix-tree (equal (uri-cst-matchp$ (tree-fix tree) elem) (uri-cst-matchp$ tree elem)))
Theorem:
(defthm uri-cst-matchp$-tree-equiv-congruence-on-tree (implies (tree-equiv tree tree-equiv) (equal (uri-cst-matchp$ tree elem) (uri-cst-matchp$ tree-equiv elem))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-matchp$-of-element-fix-elem (equal (uri-cst-matchp$ tree (element-fix elem)) (uri-cst-matchp$ tree elem)))
Theorem:
(defthm uri-cst-matchp$-element-equiv-congruence-on-elem (implies (element-equiv elem elem-equiv) (equal (uri-cst-matchp$ tree elem) (uri-cst-matchp$ tree elem-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-list-elem-matchp$ (trees elem) (declare (xargs :guard (and (tree-listp trees) (elementp elem)))) (let ((__function__ 'uri-cst-list-elem-matchp$)) (declare (ignorable __function__)) (and (tree-list-terminatedp trees) (tree-list-match-element-p trees elem *all-uri-grammar-rules*))))
Theorem:
(defthm booleanp-of-uri-cst-list-elem-matchp$ (b* ((yes/no (uri-cst-list-elem-matchp$ trees elem))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-list-elem-matchp$-of-tree-list-fix-trees (equal (uri-cst-list-elem-matchp$ (tree-list-fix trees) elem) (uri-cst-list-elem-matchp$ trees elem)))
Theorem:
(defthm uri-cst-list-elem-matchp$-tree-list-equiv-congruence-on-trees (implies (tree-list-equiv trees trees-equiv) (equal (uri-cst-list-elem-matchp$ trees elem) (uri-cst-list-elem-matchp$ trees-equiv elem))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-list-elem-matchp$-of-element-fix-elem (equal (uri-cst-list-elem-matchp$ trees (element-fix elem)) (uri-cst-list-elem-matchp$ trees elem)))
Theorem:
(defthm uri-cst-list-elem-matchp$-element-equiv-congruence-on-elem (implies (element-equiv elem elem-equiv) (equal (uri-cst-list-elem-matchp$ trees elem) (uri-cst-list-elem-matchp$ trees elem-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-list-rep-matchp$ (trees rep) (declare (xargs :guard (and (tree-listp trees) (repetitionp rep)))) (let ((__function__ 'uri-cst-list-rep-matchp$)) (declare (ignorable __function__)) (and (tree-list-terminatedp trees) (tree-list-match-repetition-p trees rep *all-uri-grammar-rules*))))
Theorem:
(defthm booleanp-of-uri-cst-list-rep-matchp$ (b* ((yes/no (uri-cst-list-rep-matchp$ trees rep))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-list-rep-matchp$-of-tree-list-fix-trees (equal (uri-cst-list-rep-matchp$ (tree-list-fix trees) rep) (uri-cst-list-rep-matchp$ trees rep)))
Theorem:
(defthm uri-cst-list-rep-matchp$-tree-list-equiv-congruence-on-trees (implies (tree-list-equiv trees trees-equiv) (equal (uri-cst-list-rep-matchp$ trees rep) (uri-cst-list-rep-matchp$ trees-equiv rep))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-list-rep-matchp$-of-repetition-fix-rep (equal (uri-cst-list-rep-matchp$ trees (repetition-fix rep)) (uri-cst-list-rep-matchp$ trees rep)))
Theorem:
(defthm uri-cst-list-rep-matchp$-repetition-equiv-congruence-on-rep (implies (repetition-equiv rep rep-equiv) (equal (uri-cst-list-rep-matchp$ trees rep) (uri-cst-list-rep-matchp$ trees rep-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-list-list-conc-matchp$ (treess conc) (declare (xargs :guard (and (tree-list-listp treess) (concatenationp conc)))) (let ((__function__ 'uri-cst-list-list-conc-matchp$)) (declare (ignorable __function__)) (and (tree-list-list-terminatedp treess) (tree-list-list-match-concatenation-p treess conc *all-uri-grammar-rules*))))
Theorem:
(defthm booleanp-of-uri-cst-list-list-conc-matchp$ (b* ((yes/no (uri-cst-list-list-conc-matchp$ treess conc))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-list-list-conc-matchp$-of-tree-list-list-fix-treess (equal (uri-cst-list-list-conc-matchp$ (tree-list-list-fix treess) conc) (uri-cst-list-list-conc-matchp$ treess conc)))
Theorem:
(defthm uri-cst-list-list-conc-matchp$-tree-list-list-equiv-congruence-on-treess (implies (tree-list-list-equiv treess treess-equiv) (equal (uri-cst-list-list-conc-matchp$ treess conc) (uri-cst-list-list-conc-matchp$ treess-equiv conc))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-list-list-conc-matchp$-of-concatenation-fix-conc (equal (uri-cst-list-list-conc-matchp$ treess (concatenation-fix conc)) (uri-cst-list-list-conc-matchp$ treess conc)))
Theorem:
(defthm uri-cst-list-list-conc-matchp$-concatenation-equiv-congruence-on-conc (implies (concatenation-equiv conc conc-equiv) (equal (uri-cst-list-list-conc-matchp$ treess conc) (uri-cst-list-list-conc-matchp$ treess conc-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-list-list-alt-matchp$ (treess alt) (declare (xargs :guard (and (tree-list-listp treess) (alternationp alt)))) (let ((__function__ 'uri-cst-list-list-alt-matchp$)) (declare (ignorable __function__)) (and (tree-list-list-terminatedp treess) (tree-list-list-match-alternation-p treess alt *all-uri-grammar-rules*))))
Theorem:
(defthm booleanp-of-uri-cst-list-list-alt-matchp$ (b* ((yes/no (uri-cst-list-list-alt-matchp$ treess alt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-list-list-alt-matchp$-of-tree-list-list-fix-treess (equal (uri-cst-list-list-alt-matchp$ (tree-list-list-fix treess) alt) (uri-cst-list-list-alt-matchp$ treess alt)))
Theorem:
(defthm uri-cst-list-list-alt-matchp$-tree-list-list-equiv-congruence-on-treess (implies (tree-list-list-equiv treess treess-equiv) (equal (uri-cst-list-list-alt-matchp$ treess alt) (uri-cst-list-list-alt-matchp$ treess-equiv alt))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-list-list-alt-matchp$-of-alternation-fix-alt (equal (uri-cst-list-list-alt-matchp$ treess (alternation-fix alt)) (uri-cst-list-list-alt-matchp$ treess alt)))
Theorem:
(defthm uri-cst-list-list-alt-matchp$-alternation-equiv-congruence-on-alt (implies (alternation-equiv alt alt-equiv) (equal (uri-cst-list-list-alt-matchp$ treess alt) (uri-cst-list-list-alt-matchp$ treess alt-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-%x30-34-nat (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "%x30-34"))) (let ((__function__ 'uri-cst-%x30-34-nat)) (declare (ignorable __function__)) (lnfix (nth 0 (tree-leafterm->get cst)))))
Theorem:
(defthm natp-of-uri-cst-%x30-34-nat (b* ((nat (uri-cst-%x30-34-nat cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-%x30-34-nat-of-tree-fix-cst (equal (uri-cst-%x30-34-nat (tree-fix cst)) (uri-cst-%x30-34-nat cst)))
Theorem:
(defthm uri-cst-%x30-34-nat-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-%x30-34-nat cst) (uri-cst-%x30-34-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-%x30-35-nat (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "%x30-35"))) (let ((__function__ 'uri-cst-%x30-35-nat)) (declare (ignorable __function__)) (lnfix (nth 0 (tree-leafterm->get cst)))))
Theorem:
(defthm natp-of-uri-cst-%x30-35-nat (b* ((nat (uri-cst-%x30-35-nat cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-%x30-35-nat-of-tree-fix-cst (equal (uri-cst-%x30-35-nat (tree-fix cst)) (uri-cst-%x30-35-nat cst)))
Theorem:
(defthm uri-cst-%x30-35-nat-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-%x30-35-nat cst) (uri-cst-%x30-35-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-%x30-39-nat (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "%x30-39"))) (let ((__function__ 'uri-cst-%x30-39-nat)) (declare (ignorable __function__)) (lnfix (nth 0 (tree-leafterm->get cst)))))
Theorem:
(defthm natp-of-uri-cst-%x30-39-nat (b* ((nat (uri-cst-%x30-39-nat cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-%x30-39-nat-of-tree-fix-cst (equal (uri-cst-%x30-39-nat (tree-fix cst)) (uri-cst-%x30-39-nat cst)))
Theorem:
(defthm uri-cst-%x30-39-nat-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-%x30-39-nat cst) (uri-cst-%x30-39-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-%x31-39-nat (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "%x31-39"))) (let ((__function__ 'uri-cst-%x31-39-nat)) (declare (ignorable __function__)) (lnfix (nth 0 (tree-leafterm->get cst)))))
Theorem:
(defthm natp-of-uri-cst-%x31-39-nat (b* ((nat (uri-cst-%x31-39-nat cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-%x31-39-nat-of-tree-fix-cst (equal (uri-cst-%x31-39-nat (tree-fix cst)) (uri-cst-%x31-39-nat cst)))
Theorem:
(defthm uri-cst-%x31-39-nat-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-%x31-39-nat cst) (uri-cst-%x31-39-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-%x41-5a-nat (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "%x41-5A"))) (let ((__function__ 'uri-cst-%x41-5a-nat)) (declare (ignorable __function__)) (lnfix (nth 0 (tree-leafterm->get cst)))))
Theorem:
(defthm natp-of-uri-cst-%x41-5a-nat (b* ((nat (uri-cst-%x41-5a-nat cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-%x41-5a-nat-of-tree-fix-cst (equal (uri-cst-%x41-5a-nat (tree-fix cst)) (uri-cst-%x41-5a-nat cst)))
Theorem:
(defthm uri-cst-%x41-5a-nat-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-%x41-5a-nat cst) (uri-cst-%x41-5a-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-%x61-7a-nat (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "%x61-7A"))) (let ((__function__ 'uri-cst-%x61-7a-nat)) (declare (ignorable __function__)) (lnfix (nth 0 (tree-leafterm->get cst)))))
Theorem:
(defthm natp-of-uri-cst-%x61-7a-nat (b* ((nat (uri-cst-%x61-7a-nat cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-%x61-7a-nat-of-tree-fix-cst (equal (uri-cst-%x61-7a-nat (tree-fix cst)) (uri-cst-%x61-7a-nat cst)))
Theorem:
(defthm uri-cst-%x61-7a-nat-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-%x61-7a-nat cst) (uri-cst-%x61-7a-nat cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-%x30-34-nat-bounds (implies (uri-cst-matchp cst "%x30-34") (and (<= 48 (uri-cst-%x30-34-nat cst)) (<= (uri-cst-%x30-34-nat cst) 52))) :rule-classes :linear)
Theorem:
(defthm uri-cst-%x30-35-nat-bounds (implies (uri-cst-matchp cst "%x30-35") (and (<= 48 (uri-cst-%x30-35-nat cst)) (<= (uri-cst-%x30-35-nat cst) 53))) :rule-classes :linear)
Theorem:
(defthm uri-cst-%x30-39-nat-bounds (implies (uri-cst-matchp cst "%x30-39") (and (<= 48 (uri-cst-%x30-39-nat cst)) (<= (uri-cst-%x30-39-nat cst) 57))) :rule-classes :linear)
Theorem:
(defthm uri-cst-%x31-39-nat-bounds (implies (uri-cst-matchp cst "%x31-39") (and (<= 49 (uri-cst-%x31-39-nat cst)) (<= (uri-cst-%x31-39-nat cst) 57))) :rule-classes :linear)
Theorem:
(defthm uri-cst-%x41-5a-nat-bounds (implies (uri-cst-matchp cst "%x41-5A") (and (<= 65 (uri-cst-%x41-5a-nat cst)) (<= (uri-cst-%x41-5a-nat cst) 90))) :rule-classes :linear)
Theorem:
(defthm uri-cst-%x61-7a-nat-bounds (implies (uri-cst-matchp cst "%x61-7A") (and (<= 97 (uri-cst-%x61-7a-nat cst)) (<= (uri-cst-%x61-7a-nat cst) 122))) :rule-classes :linear)
Theorem:
(defthm |URI-CST-"!"-LEAFTERM| (implies (uri-cst-matchp cst "\"!\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"#"-LEAFTERM| (implies (uri-cst-matchp cst "\"#\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"$"-LEAFTERM| (implies (uri-cst-matchp cst "\"$\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"%"-LEAFTERM| (implies (uri-cst-matchp cst "\"%\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"&"-LEAFTERM| (implies (uri-cst-matchp cst "\"&\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"'"-LEAFTERM| (implies (uri-cst-matchp cst "\"'\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"("-LEAFTERM| (implies (uri-cst-matchp cst "\"(\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-")"-LEAFTERM| (implies (uri-cst-matchp cst "\")\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"*"-LEAFTERM| (implies (uri-cst-matchp cst "\"*\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"+"-LEAFTERM| (implies (uri-cst-matchp cst "\"+\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-","-LEAFTERM| (implies (uri-cst-matchp cst "\",\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"-"-LEAFTERM| (implies (uri-cst-matchp cst "\"-\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"."-LEAFTERM| (implies (uri-cst-matchp cst "\".\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"/"-LEAFTERM| (implies (uri-cst-matchp cst "\"/\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"//"-LEAFTERM| (implies (uri-cst-matchp cst "\"//\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"1"-LEAFTERM| (implies (uri-cst-matchp cst "\"1\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"2"-LEAFTERM| (implies (uri-cst-matchp cst "\"2\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"25"-LEAFTERM| (implies (uri-cst-matchp cst "\"25\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-":"-LEAFTERM| (implies (uri-cst-matchp cst "\":\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"::"-LEAFTERM| (implies (uri-cst-matchp cst "\"::\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-";"-LEAFTERM| (implies (uri-cst-matchp cst "\";\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"="-LEAFTERM| (implies (uri-cst-matchp cst "\"=\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"?"-LEAFTERM| (implies (uri-cst-matchp cst "\"?\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"@"-LEAFTERM| (implies (uri-cst-matchp cst "\"@\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"A"-LEAFTERM| (implies (uri-cst-matchp cst "\"A\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"B"-LEAFTERM| (implies (uri-cst-matchp cst "\"B\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"C"-LEAFTERM| (implies (uri-cst-matchp cst "\"C\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"D"-LEAFTERM| (implies (uri-cst-matchp cst "\"D\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"E"-LEAFTERM| (implies (uri-cst-matchp cst "\"E\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"F"-LEAFTERM| (implies (uri-cst-matchp cst "\"F\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"["-LEAFTERM| (implies (uri-cst-matchp cst "\"[\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"]"-LEAFTERM| (implies (uri-cst-matchp cst "\"]\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"_"-LEAFTERM| (implies (uri-cst-matchp cst "\"_\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"v"-LEAFTERM| (implies (uri-cst-matchp cst "\"v\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm |URI-CST-"~"-LEAFTERM| (implies (uri-cst-matchp cst "\"~\"") (equal (tree-kind cst) :leafterm)))
Theorem:
(defthm uri-cst-uri-nonleaf (implies (uri-cst-matchp cst "uri") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-hier-part-nonleaf (implies (uri-cst-matchp cst "hier-part") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-uri-reference-nonleaf (implies (uri-cst-matchp cst "uri-reference") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-absolute-uri-nonleaf (implies (uri-cst-matchp cst "absolute-uri") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-relative-ref-nonleaf (implies (uri-cst-matchp cst "relative-ref") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-relative-part-nonleaf (implies (uri-cst-matchp cst "relative-part") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-scheme-nonleaf (implies (uri-cst-matchp cst "scheme") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-authority-nonleaf (implies (uri-cst-matchp cst "authority") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-userinfo-nonleaf (implies (uri-cst-matchp cst "userinfo") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-host-nonleaf (implies (uri-cst-matchp cst "host") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-port-nonleaf (implies (uri-cst-matchp cst "port") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-ip-literal-nonleaf (implies (uri-cst-matchp cst "ip-literal") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-ipvfuture-nonleaf (implies (uri-cst-matchp cst "ipvfuture") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-ipv6address-nonleaf (implies (uri-cst-matchp cst "ipv6address") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-h16-nonleaf (implies (uri-cst-matchp cst "h16") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-ls32-nonleaf (implies (uri-cst-matchp cst "ls32") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-ipv4address-nonleaf (implies (uri-cst-matchp cst "ipv4address") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-dec-octet-nonleaf (implies (uri-cst-matchp cst "dec-octet") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-reg-name-nonleaf (implies (uri-cst-matchp cst "reg-name") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-path-nonleaf (implies (uri-cst-matchp cst "path") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-path-abempty-nonleaf (implies (uri-cst-matchp cst "path-abempty") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-path-absolute-nonleaf (implies (uri-cst-matchp cst "path-absolute") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-path-noscheme-nonleaf (implies (uri-cst-matchp cst "path-noscheme") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-path-rootless-nonleaf (implies (uri-cst-matchp cst "path-rootless") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-path-empty-nonleaf (implies (uri-cst-matchp cst "path-empty") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-segment-nonleaf (implies (uri-cst-matchp cst "segment") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-segment-nz-nonleaf (implies (uri-cst-matchp cst "segment-nz") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-segment-nz-nc-nonleaf (implies (uri-cst-matchp cst "segment-nz-nc") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-pchar-nonleaf (implies (uri-cst-matchp cst "pchar") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-query-nonleaf (implies (uri-cst-matchp cst "query") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-fragment-nonleaf (implies (uri-cst-matchp cst "fragment") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-pct-encoded-nonleaf (implies (uri-cst-matchp cst "pct-encoded") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-unreserved-nonleaf (implies (uri-cst-matchp cst "unreserved") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-reserved-nonleaf (implies (uri-cst-matchp cst "reserved") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-gen-delims-nonleaf (implies (uri-cst-matchp cst "gen-delims") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-sub-delims-nonleaf (implies (uri-cst-matchp cst "sub-delims") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-alpha-nonleaf (implies (uri-cst-matchp cst "alpha") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-digit-nonleaf (implies (uri-cst-matchp cst "digit") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-hexdig-nonleaf (implies (uri-cst-matchp cst "hexdig") (equal (tree-kind cst) :nonleaf)))
Theorem:
(defthm uri-cst-uri-rulename (implies (uri-cst-matchp cst "uri") (equal (tree-nonleaf->rulename? cst) (rulename "uri"))))
Theorem:
(defthm uri-cst-hier-part-rulename (implies (uri-cst-matchp cst "hier-part") (equal (tree-nonleaf->rulename? cst) (rulename "hier-part"))))
Theorem:
(defthm uri-cst-uri-reference-rulename (implies (uri-cst-matchp cst "uri-reference") (equal (tree-nonleaf->rulename? cst) (rulename "uri-reference"))))
Theorem:
(defthm uri-cst-absolute-uri-rulename (implies (uri-cst-matchp cst "absolute-uri") (equal (tree-nonleaf->rulename? cst) (rulename "absolute-uri"))))
Theorem:
(defthm uri-cst-relative-ref-rulename (implies (uri-cst-matchp cst "relative-ref") (equal (tree-nonleaf->rulename? cst) (rulename "relative-ref"))))
Theorem:
(defthm uri-cst-relative-part-rulename (implies (uri-cst-matchp cst "relative-part") (equal (tree-nonleaf->rulename? cst) (rulename "relative-part"))))
Theorem:
(defthm uri-cst-scheme-rulename (implies (uri-cst-matchp cst "scheme") (equal (tree-nonleaf->rulename? cst) (rulename "scheme"))))
Theorem:
(defthm uri-cst-authority-rulename (implies (uri-cst-matchp cst "authority") (equal (tree-nonleaf->rulename? cst) (rulename "authority"))))
Theorem:
(defthm uri-cst-userinfo-rulename (implies (uri-cst-matchp cst "userinfo") (equal (tree-nonleaf->rulename? cst) (rulename "userinfo"))))
Theorem:
(defthm uri-cst-host-rulename (implies (uri-cst-matchp cst "host") (equal (tree-nonleaf->rulename? cst) (rulename "host"))))
Theorem:
(defthm uri-cst-port-rulename (implies (uri-cst-matchp cst "port") (equal (tree-nonleaf->rulename? cst) (rulename "port"))))
Theorem:
(defthm uri-cst-ip-literal-rulename (implies (uri-cst-matchp cst "ip-literal") (equal (tree-nonleaf->rulename? cst) (rulename "ip-literal"))))
Theorem:
(defthm uri-cst-ipvfuture-rulename (implies (uri-cst-matchp cst "ipvfuture") (equal (tree-nonleaf->rulename? cst) (rulename "ipvfuture"))))
Theorem:
(defthm uri-cst-ipv6address-rulename (implies (uri-cst-matchp cst "ipv6address") (equal (tree-nonleaf->rulename? cst) (rulename "ipv6address"))))
Theorem:
(defthm uri-cst-h16-rulename (implies (uri-cst-matchp cst "h16") (equal (tree-nonleaf->rulename? cst) (rulename "h16"))))
Theorem:
(defthm uri-cst-ls32-rulename (implies (uri-cst-matchp cst "ls32") (equal (tree-nonleaf->rulename? cst) (rulename "ls32"))))
Theorem:
(defthm uri-cst-ipv4address-rulename (implies (uri-cst-matchp cst "ipv4address") (equal (tree-nonleaf->rulename? cst) (rulename "ipv4address"))))
Theorem:
(defthm uri-cst-dec-octet-rulename (implies (uri-cst-matchp cst "dec-octet") (equal (tree-nonleaf->rulename? cst) (rulename "dec-octet"))))
Theorem:
(defthm uri-cst-reg-name-rulename (implies (uri-cst-matchp cst "reg-name") (equal (tree-nonleaf->rulename? cst) (rulename "reg-name"))))
Theorem:
(defthm uri-cst-path-rulename (implies (uri-cst-matchp cst "path") (equal (tree-nonleaf->rulename? cst) (rulename "path"))))
Theorem:
(defthm uri-cst-path-abempty-rulename (implies (uri-cst-matchp cst "path-abempty") (equal (tree-nonleaf->rulename? cst) (rulename "path-abempty"))))
Theorem:
(defthm uri-cst-path-absolute-rulename (implies (uri-cst-matchp cst "path-absolute") (equal (tree-nonleaf->rulename? cst) (rulename "path-absolute"))))
Theorem:
(defthm uri-cst-path-noscheme-rulename (implies (uri-cst-matchp cst "path-noscheme") (equal (tree-nonleaf->rulename? cst) (rulename "path-noscheme"))))
Theorem:
(defthm uri-cst-path-rootless-rulename (implies (uri-cst-matchp cst "path-rootless") (equal (tree-nonleaf->rulename? cst) (rulename "path-rootless"))))
Theorem:
(defthm uri-cst-path-empty-rulename (implies (uri-cst-matchp cst "path-empty") (equal (tree-nonleaf->rulename? cst) (rulename "path-empty"))))
Theorem:
(defthm uri-cst-segment-rulename (implies (uri-cst-matchp cst "segment") (equal (tree-nonleaf->rulename? cst) (rulename "segment"))))
Theorem:
(defthm uri-cst-segment-nz-rulename (implies (uri-cst-matchp cst "segment-nz") (equal (tree-nonleaf->rulename? cst) (rulename "segment-nz"))))
Theorem:
(defthm uri-cst-segment-nz-nc-rulename (implies (uri-cst-matchp cst "segment-nz-nc") (equal (tree-nonleaf->rulename? cst) (rulename "segment-nz-nc"))))
Theorem:
(defthm uri-cst-pchar-rulename (implies (uri-cst-matchp cst "pchar") (equal (tree-nonleaf->rulename? cst) (rulename "pchar"))))
Theorem:
(defthm uri-cst-query-rulename (implies (uri-cst-matchp cst "query") (equal (tree-nonleaf->rulename? cst) (rulename "query"))))
Theorem:
(defthm uri-cst-fragment-rulename (implies (uri-cst-matchp cst "fragment") (equal (tree-nonleaf->rulename? cst) (rulename "fragment"))))
Theorem:
(defthm uri-cst-pct-encoded-rulename (implies (uri-cst-matchp cst "pct-encoded") (equal (tree-nonleaf->rulename? cst) (rulename "pct-encoded"))))
Theorem:
(defthm uri-cst-unreserved-rulename (implies (uri-cst-matchp cst "unreserved") (equal (tree-nonleaf->rulename? cst) (rulename "unreserved"))))
Theorem:
(defthm uri-cst-reserved-rulename (implies (uri-cst-matchp cst "reserved") (equal (tree-nonleaf->rulename? cst) (rulename "reserved"))))
Theorem:
(defthm uri-cst-gen-delims-rulename (implies (uri-cst-matchp cst "gen-delims") (equal (tree-nonleaf->rulename? cst) (rulename "gen-delims"))))
Theorem:
(defthm uri-cst-sub-delims-rulename (implies (uri-cst-matchp cst "sub-delims") (equal (tree-nonleaf->rulename? cst) (rulename "sub-delims"))))
Theorem:
(defthm uri-cst-alpha-rulename (implies (uri-cst-matchp cst "alpha") (equal (tree-nonleaf->rulename? cst) (rulename "alpha"))))
Theorem:
(defthm uri-cst-digit-rulename (implies (uri-cst-matchp cst "digit") (equal (tree-nonleaf->rulename? cst) (rulename "digit"))))
Theorem:
(defthm uri-cst-hexdig-rulename (implies (uri-cst-matchp cst "hexdig") (equal (tree-nonleaf->rulename? cst) (rulename "hexdig"))))
Theorem:
(defthm uri-cst-uri-branches-match-alt (implies (uri-cst-matchp cst "uri") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "scheme \":\" hier-part [ \"?\" query ] [ \"#\" fragment ]")))
Theorem:
(defthm uri-cst-hier-part-branches-match-alt (implies (uri-cst-matchp cst "hier-part") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "\"//\" authority path-abempty / path-absolute / path-rootless / path-empty")))
Theorem:
(defthm uri-cst-uri-reference-branches-match-alt (implies (uri-cst-matchp cst "uri-reference") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "uri / relative-ref")))
Theorem:
(defthm uri-cst-absolute-uri-branches-match-alt (implies (uri-cst-matchp cst "absolute-uri") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "scheme \":\" hier-part [ \"?\" query ]")))
Theorem:
(defthm uri-cst-relative-ref-branches-match-alt (implies (uri-cst-matchp cst "relative-ref") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "relative-part [ \"?\" query ] [ \"#\" fragment ]")))
Theorem:
(defthm uri-cst-relative-part-branches-match-alt (implies (uri-cst-matchp cst "relative-part") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "\"//\" authority path-abempty / path-absolute / path-noscheme / path-empty")))
Theorem:
(defthm uri-cst-scheme-branches-match-alt (implies (uri-cst-matchp cst "scheme") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "alpha *( alpha / digit / \"+\" / \"-\" / \".\" )")))
Theorem:
(defthm uri-cst-authority-branches-match-alt (implies (uri-cst-matchp cst "authority") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "[ userinfo \"@\" ] host [ \":\" port ]")))
Theorem:
(defthm uri-cst-userinfo-branches-match-alt (implies (uri-cst-matchp cst "userinfo") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "*( unreserved / pct-encoded / sub-delims / \":\" )")))
Theorem:
(defthm uri-cst-host-branches-match-alt (implies (uri-cst-matchp cst "host") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "ip-literal / ipv4address / reg-name")))
Theorem:
(defthm uri-cst-port-branches-match-alt (implies (uri-cst-matchp cst "port") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "*digit")))
Theorem:
(defthm uri-cst-ip-literal-branches-match-alt (implies (uri-cst-matchp cst "ip-literal") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "\"[\" ( ipv6address / ipvfuture ) \"]\"")))
Theorem:
(defthm uri-cst-ipvfuture-branches-match-alt (implies (uri-cst-matchp cst "ipvfuture") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "\"v\" 1*hexdig \".\" 1*( unreserved / sub-delims / \":\" )")))
Theorem:
(defthm uri-cst-ipv6address-branches-match-alt (implies (uri-cst-matchp cst "ipv6address") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "6( h16 \":\" ) ls32 / \"::\" 5( h16 \":\" ) ls32 / [ h16 ] \"::\" 4( h16 \":\" ) ls32 / [ *1( h16 \":\" ) h16 ] \"::\" 3( h16 \":\" ) ls32 / [ *2( h16 \":\" ) h16 ] \"::\" 2( h16 \":\" ) ls32 / [ *3( h16 \":\" ) h16 ] \"::\" h16 \":\" ls32 / [ *4( h16 \":\" ) h16 ] \"::\" ls32 / [ *5( h16 \":\" ) h16 ] \"::\" h16 / [ *6( h16 \":\" ) h16 ] \"::\"")))
Theorem:
(defthm uri-cst-h16-branches-match-alt (implies (uri-cst-matchp cst "h16") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "1*4hexdig")))
Theorem:
(defthm uri-cst-ls32-branches-match-alt (implies (uri-cst-matchp cst "ls32") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "( h16 \":\" h16 ) / ipv4address")))
Theorem:
(defthm uri-cst-ipv4address-branches-match-alt (implies (uri-cst-matchp cst "ipv4address") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "dec-octet \".\" dec-octet \".\" dec-octet \".\" dec-octet")))
Theorem:
(defthm uri-cst-dec-octet-branches-match-alt (implies (uri-cst-matchp cst "dec-octet") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "digit / %x31-39 digit / \"1\" 2digit / \"2\" %x30-34 digit / \"25\" %x30-35")))
Theorem:
(defthm uri-cst-reg-name-branches-match-alt (implies (uri-cst-matchp cst "reg-name") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "*( unreserved / pct-encoded / sub-delims )")))
Theorem:
(defthm uri-cst-path-branches-match-alt (implies (uri-cst-matchp cst "path") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "path-abempty / path-absolute / path-noscheme / path-rootless / path-empty")))
Theorem:
(defthm uri-cst-path-abempty-branches-match-alt (implies (uri-cst-matchp cst "path-abempty") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "*( \"/\" segment )")))
Theorem:
(defthm uri-cst-path-absolute-branches-match-alt (implies (uri-cst-matchp cst "path-absolute") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "\"/\" [ segment-nz *( \"/\" segment ) ]")))
Theorem:
(defthm uri-cst-path-noscheme-branches-match-alt (implies (uri-cst-matchp cst "path-noscheme") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "segment-nz-nc *( \"/\" segment )")))
Theorem:
(defthm uri-cst-path-rootless-branches-match-alt (implies (uri-cst-matchp cst "path-rootless") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "segment-nz *( \"/\" segment )")))
Theorem:
(defthm uri-cst-path-empty-branches-match-alt (implies (uri-cst-matchp cst "path-empty") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "0<pchar>")))
Theorem:
(defthm uri-cst-segment-branches-match-alt (implies (uri-cst-matchp cst "segment") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "*pchar")))
Theorem:
(defthm uri-cst-segment-nz-branches-match-alt (implies (uri-cst-matchp cst "segment-nz") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "1*pchar")))
Theorem:
(defthm uri-cst-segment-nz-nc-branches-match-alt (implies (uri-cst-matchp cst "segment-nz-nc") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "1*( unreserved / pct-encoded / sub-delims / \"@\" )")))
Theorem:
(defthm uri-cst-pchar-branches-match-alt (implies (uri-cst-matchp cst "pchar") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "unreserved / pct-encoded / sub-delims / \":\" / \"@\"")))
Theorem:
(defthm uri-cst-query-branches-match-alt (implies (uri-cst-matchp cst "query") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "*( pchar / \"/\" / \"?\" )")))
Theorem:
(defthm uri-cst-fragment-branches-match-alt (implies (uri-cst-matchp cst "fragment") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "*( pchar / \"/\" / \"?\" )")))
Theorem:
(defthm uri-cst-pct-encoded-branches-match-alt (implies (uri-cst-matchp cst "pct-encoded") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "\"%\" hexdig hexdig")))
Theorem:
(defthm uri-cst-unreserved-branches-match-alt (implies (uri-cst-matchp cst "unreserved") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "alpha / digit / \"-\" / \".\" / \"_\" / \"~\"")))
Theorem:
(defthm uri-cst-reserved-branches-match-alt (implies (uri-cst-matchp cst "reserved") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "gen-delims / sub-delims")))
Theorem:
(defthm uri-cst-gen-delims-branches-match-alt (implies (uri-cst-matchp cst "gen-delims") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "\":\" / \"/\" / \"?\" / \"#\" / \"[\" / \"]\" / \"@\"")))
Theorem:
(defthm uri-cst-sub-delims-branches-match-alt (implies (uri-cst-matchp cst "sub-delims") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "\"!\" / \"$\" / \"&\" / \"'\" / \"(\" / \")\" / \"*\" / \"+\" / \",\" / \";\" / \"=\"")))
Theorem:
(defthm uri-cst-alpha-branches-match-alt (implies (uri-cst-matchp cst "alpha") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "%x41-5A / %x61-7A")))
Theorem:
(defthm uri-cst-digit-branches-match-alt (implies (uri-cst-matchp cst "digit") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "%x30-39")))
Theorem:
(defthm uri-cst-hexdig-branches-match-alt (implies (uri-cst-matchp cst "hexdig") (uri-cst-list-list-alt-matchp (tree-nonleaf->branches cst) "digit / \"A\" / \"B\" / \"C\" / \"D\" / \"E\" / \"F\"")))
Theorem:
(defthm uri-cst-uri-concs (implies (uri-cst-list-list-alt-matchp cstss "scheme \":\" hier-part [ \"?\" query ] [ \"#\" fragment ]") (or (uri-cst-list-list-conc-matchp cstss "scheme \":\" hier-part [ \"?\" query ] [ \"#\" fragment ]"))))
Theorem:
(defthm uri-cst-hier-part-concs (implies (uri-cst-list-list-alt-matchp cstss "\"//\" authority path-abempty / path-absolute / path-rootless / path-empty") (or (uri-cst-list-list-conc-matchp cstss "\"//\" authority path-abempty") (uri-cst-list-list-conc-matchp cstss "path-absolute") (uri-cst-list-list-conc-matchp cstss "path-rootless") (uri-cst-list-list-conc-matchp cstss "path-empty"))))
Theorem:
(defthm uri-cst-uri-reference-concs (implies (uri-cst-list-list-alt-matchp cstss "uri / relative-ref") (or (uri-cst-list-list-conc-matchp cstss "uri") (uri-cst-list-list-conc-matchp cstss "relative-ref"))))
Theorem:
(defthm uri-cst-absolute-uri-concs (implies (uri-cst-list-list-alt-matchp cstss "scheme \":\" hier-part [ \"?\" query ]") (or (uri-cst-list-list-conc-matchp cstss "scheme \":\" hier-part [ \"?\" query ]"))))
Theorem:
(defthm uri-cst-relative-ref-concs (implies (uri-cst-list-list-alt-matchp cstss "relative-part [ \"?\" query ] [ \"#\" fragment ]") (or (uri-cst-list-list-conc-matchp cstss "relative-part [ \"?\" query ] [ \"#\" fragment ]"))))
Theorem:
(defthm uri-cst-relative-part-concs (implies (uri-cst-list-list-alt-matchp cstss "\"//\" authority path-abempty / path-absolute / path-noscheme / path-empty") (or (uri-cst-list-list-conc-matchp cstss "\"//\" authority path-abempty") (uri-cst-list-list-conc-matchp cstss "path-absolute") (uri-cst-list-list-conc-matchp cstss "path-noscheme") (uri-cst-list-list-conc-matchp cstss "path-empty"))))
Theorem:
(defthm uri-cst-scheme-concs (implies (uri-cst-list-list-alt-matchp cstss "alpha *( alpha / digit / \"+\" / \"-\" / \".\" )") (or (uri-cst-list-list-conc-matchp cstss "alpha *( alpha / digit / \"+\" / \"-\" / \".\" )"))))
Theorem:
(defthm uri-cst-authority-concs (implies (uri-cst-list-list-alt-matchp cstss "[ userinfo \"@\" ] host [ \":\" port ]") (or (uri-cst-list-list-conc-matchp cstss "[ userinfo \"@\" ] host [ \":\" port ]"))))
Theorem:
(defthm uri-cst-userinfo-concs (implies (uri-cst-list-list-alt-matchp cstss "*( unreserved / pct-encoded / sub-delims / \":\" )") (or (uri-cst-list-list-conc-matchp cstss "*( unreserved / pct-encoded / sub-delims / \":\" )"))))
Theorem:
(defthm uri-cst-host-concs (implies (uri-cst-list-list-alt-matchp cstss "ip-literal / ipv4address / reg-name") (or (uri-cst-list-list-conc-matchp cstss "ip-literal") (uri-cst-list-list-conc-matchp cstss "ipv4address") (uri-cst-list-list-conc-matchp cstss "reg-name"))))
Theorem:
(defthm uri-cst-port-concs (implies (uri-cst-list-list-alt-matchp cstss "*digit") (or (uri-cst-list-list-conc-matchp cstss "*digit"))))
Theorem:
(defthm uri-cst-ip-literal-concs (implies (uri-cst-list-list-alt-matchp cstss "\"[\" ( ipv6address / ipvfuture ) \"]\"") (or (uri-cst-list-list-conc-matchp cstss "\"[\" ( ipv6address / ipvfuture ) \"]\""))))
Theorem:
(defthm uri-cst-ipvfuture-concs (implies (uri-cst-list-list-alt-matchp cstss "\"v\" 1*hexdig \".\" 1*( unreserved / sub-delims / \":\" )") (or (uri-cst-list-list-conc-matchp cstss "\"v\" 1*hexdig \".\" 1*( unreserved / sub-delims / \":\" )"))))
Theorem:
(defthm uri-cst-ipv6address-concs (implies (uri-cst-list-list-alt-matchp cstss "6( h16 \":\" ) ls32 / \"::\" 5( h16 \":\" ) ls32 / [ h16 ] \"::\" 4( h16 \":\" ) ls32 / [ *1( h16 \":\" ) h16 ] \"::\" 3( h16 \":\" ) ls32 / [ *2( h16 \":\" ) h16 ] \"::\" 2( h16 \":\" ) ls32 / [ *3( h16 \":\" ) h16 ] \"::\" h16 \":\" ls32 / [ *4( h16 \":\" ) h16 ] \"::\" ls32 / [ *5( h16 \":\" ) h16 ] \"::\" h16 / [ *6( h16 \":\" ) h16 ] \"::\"") (or (uri-cst-list-list-conc-matchp cstss "6( h16 \":\" ) ls32") (uri-cst-list-list-conc-matchp cstss "\"::\" 5( h16 \":\" ) ls32") (uri-cst-list-list-conc-matchp cstss "[ h16 ] \"::\" 4( h16 \":\" ) ls32") (uri-cst-list-list-conc-matchp cstss "[ *1( h16 \":\" ) h16 ] \"::\" 3( h16 \":\" ) ls32") (uri-cst-list-list-conc-matchp cstss "[ *2( h16 \":\" ) h16 ] \"::\" 2( h16 \":\" ) ls32") (uri-cst-list-list-conc-matchp cstss "[ *3( h16 \":\" ) h16 ] \"::\" h16 \":\" ls32") (uri-cst-list-list-conc-matchp cstss "[ *4( h16 \":\" ) h16 ] \"::\" ls32") (uri-cst-list-list-conc-matchp cstss "[ *5( h16 \":\" ) h16 ] \"::\" h16") (uri-cst-list-list-conc-matchp cstss "[ *6( h16 \":\" ) h16 ] \"::\""))))
Theorem:
(defthm uri-cst-h16-concs (implies (uri-cst-list-list-alt-matchp cstss "1*4hexdig") (or (uri-cst-list-list-conc-matchp cstss "1*4hexdig"))))
Theorem:
(defthm uri-cst-ls32-concs (implies (uri-cst-list-list-alt-matchp cstss "( h16 \":\" h16 ) / ipv4address") (or (uri-cst-list-list-conc-matchp cstss "( h16 \":\" h16 )") (uri-cst-list-list-conc-matchp cstss "ipv4address"))))
Theorem:
(defthm uri-cst-ipv4address-concs (implies (uri-cst-list-list-alt-matchp cstss "dec-octet \".\" dec-octet \".\" dec-octet \".\" dec-octet") (or (uri-cst-list-list-conc-matchp cstss "dec-octet \".\" dec-octet \".\" dec-octet \".\" dec-octet"))))
Theorem:
(defthm uri-cst-dec-octet-concs (implies (uri-cst-list-list-alt-matchp cstss "digit / %x31-39 digit / \"1\" 2digit / \"2\" %x30-34 digit / \"25\" %x30-35") (or (uri-cst-list-list-conc-matchp cstss "digit") (uri-cst-list-list-conc-matchp cstss "%x31-39 digit") (uri-cst-list-list-conc-matchp cstss "\"1\" 2digit") (uri-cst-list-list-conc-matchp cstss "\"2\" %x30-34 digit") (uri-cst-list-list-conc-matchp cstss "\"25\" %x30-35"))))
Theorem:
(defthm uri-cst-reg-name-concs (implies (uri-cst-list-list-alt-matchp cstss "*( unreserved / pct-encoded / sub-delims )") (or (uri-cst-list-list-conc-matchp cstss "*( unreserved / pct-encoded / sub-delims )"))))
Theorem:
(defthm uri-cst-path-concs (implies (uri-cst-list-list-alt-matchp cstss "path-abempty / path-absolute / path-noscheme / path-rootless / path-empty") (or (uri-cst-list-list-conc-matchp cstss "path-abempty") (uri-cst-list-list-conc-matchp cstss "path-absolute") (uri-cst-list-list-conc-matchp cstss "path-noscheme") (uri-cst-list-list-conc-matchp cstss "path-rootless") (uri-cst-list-list-conc-matchp cstss "path-empty"))))
Theorem:
(defthm uri-cst-path-abempty-concs (implies (uri-cst-list-list-alt-matchp cstss "*( \"/\" segment )") (or (uri-cst-list-list-conc-matchp cstss "*( \"/\" segment )"))))
Theorem:
(defthm uri-cst-path-absolute-concs (implies (uri-cst-list-list-alt-matchp cstss "\"/\" [ segment-nz *( \"/\" segment ) ]") (or (uri-cst-list-list-conc-matchp cstss "\"/\" [ segment-nz *( \"/\" segment ) ]"))))
Theorem:
(defthm uri-cst-path-noscheme-concs (implies (uri-cst-list-list-alt-matchp cstss "segment-nz-nc *( \"/\" segment )") (or (uri-cst-list-list-conc-matchp cstss "segment-nz-nc *( \"/\" segment )"))))
Theorem:
(defthm uri-cst-path-rootless-concs (implies (uri-cst-list-list-alt-matchp cstss "segment-nz *( \"/\" segment )") (or (uri-cst-list-list-conc-matchp cstss "segment-nz *( \"/\" segment )"))))
Theorem:
(defthm uri-cst-path-empty-concs (implies (uri-cst-list-list-alt-matchp cstss "0<pchar>") (or (uri-cst-list-list-conc-matchp cstss "0<pchar>"))))
Theorem:
(defthm uri-cst-segment-concs (implies (uri-cst-list-list-alt-matchp cstss "*pchar") (or (uri-cst-list-list-conc-matchp cstss "*pchar"))))
Theorem:
(defthm uri-cst-segment-nz-concs (implies (uri-cst-list-list-alt-matchp cstss "1*pchar") (or (uri-cst-list-list-conc-matchp cstss "1*pchar"))))
Theorem:
(defthm uri-cst-segment-nz-nc-concs (implies (uri-cst-list-list-alt-matchp cstss "1*( unreserved / pct-encoded / sub-delims / \"@\" )") (or (uri-cst-list-list-conc-matchp cstss "1*( unreserved / pct-encoded / sub-delims / \"@\" )"))))
Theorem:
(defthm uri-cst-pchar-concs (implies (uri-cst-list-list-alt-matchp cstss "unreserved / pct-encoded / sub-delims / \":\" / \"@\"") (or (uri-cst-list-list-conc-matchp cstss "unreserved") (uri-cst-list-list-conc-matchp cstss "pct-encoded") (uri-cst-list-list-conc-matchp cstss "sub-delims") (uri-cst-list-list-conc-matchp cstss "\":\"") (uri-cst-list-list-conc-matchp cstss "\"@\""))))
Theorem:
(defthm uri-cst-query-concs (implies (uri-cst-list-list-alt-matchp cstss "*( pchar / \"/\" / \"?\" )") (or (uri-cst-list-list-conc-matchp cstss "*( pchar / \"/\" / \"?\" )"))))
Theorem:
(defthm uri-cst-fragment-concs (implies (uri-cst-list-list-alt-matchp cstss "*( pchar / \"/\" / \"?\" )") (or (uri-cst-list-list-conc-matchp cstss "*( pchar / \"/\" / \"?\" )"))))
Theorem:
(defthm uri-cst-pct-encoded-concs (implies (uri-cst-list-list-alt-matchp cstss "\"%\" hexdig hexdig") (or (uri-cst-list-list-conc-matchp cstss "\"%\" hexdig hexdig"))))
Theorem:
(defthm uri-cst-unreserved-concs (implies (uri-cst-list-list-alt-matchp cstss "alpha / digit / \"-\" / \".\" / \"_\" / \"~\"") (or (uri-cst-list-list-conc-matchp cstss "alpha") (uri-cst-list-list-conc-matchp cstss "digit") (uri-cst-list-list-conc-matchp cstss "\"-\"") (uri-cst-list-list-conc-matchp cstss "\".\"") (uri-cst-list-list-conc-matchp cstss "\"_\"") (uri-cst-list-list-conc-matchp cstss "\"~\""))))
Theorem:
(defthm uri-cst-reserved-concs (implies (uri-cst-list-list-alt-matchp cstss "gen-delims / sub-delims") (or (uri-cst-list-list-conc-matchp cstss "gen-delims") (uri-cst-list-list-conc-matchp cstss "sub-delims"))))
Theorem:
(defthm uri-cst-gen-delims-concs (implies (uri-cst-list-list-alt-matchp cstss "\":\" / \"/\" / \"?\" / \"#\" / \"[\" / \"]\" / \"@\"") (or (uri-cst-list-list-conc-matchp cstss "\":\"") (uri-cst-list-list-conc-matchp cstss "\"/\"") (uri-cst-list-list-conc-matchp cstss "\"?\"") (uri-cst-list-list-conc-matchp cstss "\"#\"") (uri-cst-list-list-conc-matchp cstss "\"[\"") (uri-cst-list-list-conc-matchp cstss "\"]\"") (uri-cst-list-list-conc-matchp cstss "\"@\""))))
Theorem:
(defthm uri-cst-sub-delims-concs (implies (uri-cst-list-list-alt-matchp cstss "\"!\" / \"$\" / \"&\" / \"'\" / \"(\" / \")\" / \"*\" / \"+\" / \",\" / \";\" / \"=\"") (or (uri-cst-list-list-conc-matchp cstss "\"!\"") (uri-cst-list-list-conc-matchp cstss "\"$\"") (uri-cst-list-list-conc-matchp cstss "\"&\"") (uri-cst-list-list-conc-matchp cstss "\"'\"") (uri-cst-list-list-conc-matchp cstss "\"(\"") (uri-cst-list-list-conc-matchp cstss "\")\"") (uri-cst-list-list-conc-matchp cstss "\"*\"") (uri-cst-list-list-conc-matchp cstss "\"+\"") (uri-cst-list-list-conc-matchp cstss "\",\"") (uri-cst-list-list-conc-matchp cstss "\";\"") (uri-cst-list-list-conc-matchp cstss "\"=\""))))
Theorem:
(defthm uri-cst-alpha-concs (implies (uri-cst-list-list-alt-matchp cstss "%x41-5A / %x61-7A") (or (uri-cst-list-list-conc-matchp cstss "%x41-5A") (uri-cst-list-list-conc-matchp cstss "%x61-7A"))))
Theorem:
(defthm uri-cst-digit-concs (implies (uri-cst-list-list-alt-matchp cstss "%x30-39") (or (uri-cst-list-list-conc-matchp cstss "%x30-39"))))
Theorem:
(defthm uri-cst-hexdig-concs (implies (uri-cst-list-list-alt-matchp cstss "digit / \"A\" / \"B\" / \"C\" / \"D\" / \"E\" / \"F\"") (or (uri-cst-list-list-conc-matchp cstss "digit") (uri-cst-list-list-conc-matchp cstss "\"A\"") (uri-cst-list-list-conc-matchp cstss "\"B\"") (uri-cst-list-list-conc-matchp cstss "\"C\"") (uri-cst-list-list-conc-matchp cstss "\"D\"") (uri-cst-list-list-conc-matchp cstss "\"E\"") (uri-cst-list-list-conc-matchp cstss "\"F\""))))
Theorem:
(defthm uri-cst-hier-part-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "path-absolute") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-absolute"))))
Theorem:
(defthm uri-cst-hier-part-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "path-rootless") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-rootless"))))
Theorem:
(defthm uri-cst-hier-part-conc4-matching (implies (uri-cst-list-list-conc-matchp cstss "path-empty") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-empty"))))
Theorem:
(defthm uri-cst-uri-reference-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "uri") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "uri"))))
Theorem:
(defthm uri-cst-uri-reference-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "relative-ref") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "relative-ref"))))
Theorem:
(defthm uri-cst-relative-part-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "path-absolute") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-absolute"))))
Theorem:
(defthm uri-cst-relative-part-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "path-noscheme") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-noscheme"))))
Theorem:
(defthm uri-cst-relative-part-conc4-matching (implies (uri-cst-list-list-conc-matchp cstss "path-empty") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-empty"))))
Theorem:
(defthm uri-cst-userinfo-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "*( unreserved / pct-encoded / sub-delims / \":\" )") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "*( unreserved / pct-encoded / sub-delims / \":\" )"))))
Theorem:
(defthm uri-cst-host-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "ip-literal") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "ip-literal"))))
Theorem:
(defthm uri-cst-host-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "ipv4address") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "ipv4address"))))
Theorem:
(defthm uri-cst-host-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "reg-name") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "reg-name"))))
Theorem:
(defthm uri-cst-port-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "*digit") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "*digit"))))
Theorem:
(defthm uri-cst-h16-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "1*4hexdig") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "1*4hexdig"))))
Theorem:
(defthm uri-cst-ls32-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "( h16 \":\" h16 )") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "( h16 \":\" h16 )"))))
Theorem:
(defthm uri-cst-ls32-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "ipv4address") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "ipv4address"))))
Theorem:
(defthm uri-cst-dec-octet-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "digit") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "digit"))))
Theorem:
(defthm uri-cst-reg-name-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "*( unreserved / pct-encoded / sub-delims )") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "*( unreserved / pct-encoded / sub-delims )"))))
Theorem:
(defthm uri-cst-path-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "path-abempty") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-abempty"))))
Theorem:
(defthm uri-cst-path-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "path-absolute") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-absolute"))))
Theorem:
(defthm uri-cst-path-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "path-noscheme") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-noscheme"))))
Theorem:
(defthm uri-cst-path-conc4-matching (implies (uri-cst-list-list-conc-matchp cstss "path-rootless") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-rootless"))))
Theorem:
(defthm uri-cst-path-conc5-matching (implies (uri-cst-list-list-conc-matchp cstss "path-empty") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "path-empty"))))
Theorem:
(defthm uri-cst-path-abempty-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "*( \"/\" segment )") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "*( \"/\" segment )"))))
Theorem:
(defthm uri-cst-path-empty-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "0<pchar>") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "0<pchar>"))))
Theorem:
(defthm uri-cst-segment-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "*pchar") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "*pchar"))))
Theorem:
(defthm uri-cst-segment-nz-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "1*pchar") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "1*pchar"))))
Theorem:
(defthm uri-cst-segment-nz-nc-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "1*( unreserved / pct-encoded / sub-delims / \"@\" )") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "1*( unreserved / pct-encoded / sub-delims / \"@\" )"))))
Theorem:
(defthm uri-cst-pchar-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "unreserved") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "unreserved"))))
Theorem:
(defthm uri-cst-pchar-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "pct-encoded") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "pct-encoded"))))
Theorem:
(defthm uri-cst-pchar-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "sub-delims") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "sub-delims"))))
Theorem:
(defthm uri-cst-pchar-conc4-matching (implies (uri-cst-list-list-conc-matchp cstss "\":\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\":\""))))
Theorem:
(defthm uri-cst-pchar-conc5-matching (implies (uri-cst-list-list-conc-matchp cstss "\"@\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"@\""))))
Theorem:
(defthm uri-cst-query-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "*( pchar / \"/\" / \"?\" )") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "*( pchar / \"/\" / \"?\" )"))))
Theorem:
(defthm uri-cst-fragment-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "*( pchar / \"/\" / \"?\" )") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "*( pchar / \"/\" / \"?\" )"))))
Theorem:
(defthm uri-cst-unreserved-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "alpha") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "alpha"))))
Theorem:
(defthm uri-cst-unreserved-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "digit") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "digit"))))
Theorem:
(defthm uri-cst-unreserved-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "\"-\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"-\""))))
Theorem:
(defthm uri-cst-unreserved-conc4-matching (implies (uri-cst-list-list-conc-matchp cstss "\".\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\".\""))))
Theorem:
(defthm uri-cst-unreserved-conc5-matching (implies (uri-cst-list-list-conc-matchp cstss "\"_\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"_\""))))
Theorem:
(defthm uri-cst-unreserved-conc6-matching (implies (uri-cst-list-list-conc-matchp cstss "\"~\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"~\""))))
Theorem:
(defthm uri-cst-reserved-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "gen-delims") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "gen-delims"))))
Theorem:
(defthm uri-cst-reserved-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "sub-delims") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "sub-delims"))))
Theorem:
(defthm uri-cst-gen-delims-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "\":\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\":\""))))
Theorem:
(defthm uri-cst-gen-delims-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "\"/\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"/\""))))
Theorem:
(defthm uri-cst-gen-delims-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "\"?\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"?\""))))
Theorem:
(defthm uri-cst-gen-delims-conc4-matching (implies (uri-cst-list-list-conc-matchp cstss "\"#\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"#\""))))
Theorem:
(defthm uri-cst-gen-delims-conc5-matching (implies (uri-cst-list-list-conc-matchp cstss "\"[\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"[\""))))
Theorem:
(defthm uri-cst-gen-delims-conc6-matching (implies (uri-cst-list-list-conc-matchp cstss "\"]\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"]\""))))
Theorem:
(defthm uri-cst-gen-delims-conc7-matching (implies (uri-cst-list-list-conc-matchp cstss "\"@\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"@\""))))
Theorem:
(defthm uri-cst-sub-delims-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "\"!\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"!\""))))
Theorem:
(defthm uri-cst-sub-delims-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "\"$\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"$\""))))
Theorem:
(defthm uri-cst-sub-delims-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "\"&\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"&\""))))
Theorem:
(defthm uri-cst-sub-delims-conc4-matching (implies (uri-cst-list-list-conc-matchp cstss "\"'\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"'\""))))
Theorem:
(defthm uri-cst-sub-delims-conc5-matching (implies (uri-cst-list-list-conc-matchp cstss "\"(\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"(\""))))
Theorem:
(defthm uri-cst-sub-delims-conc6-matching (implies (uri-cst-list-list-conc-matchp cstss "\")\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\")\""))))
Theorem:
(defthm uri-cst-sub-delims-conc7-matching (implies (uri-cst-list-list-conc-matchp cstss "\"*\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"*\""))))
Theorem:
(defthm uri-cst-sub-delims-conc8-matching (implies (uri-cst-list-list-conc-matchp cstss "\"+\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"+\""))))
Theorem:
(defthm uri-cst-sub-delims-conc9-matching (implies (uri-cst-list-list-conc-matchp cstss "\",\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\",\""))))
Theorem:
(defthm uri-cst-sub-delims-conc10-matching (implies (uri-cst-list-list-conc-matchp cstss "\";\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\";\""))))
Theorem:
(defthm uri-cst-sub-delims-conc11-matching (implies (uri-cst-list-list-conc-matchp cstss "\"=\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"=\""))))
Theorem:
(defthm uri-cst-alpha-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "%x41-5A") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "%x41-5A"))))
Theorem:
(defthm uri-cst-alpha-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "%x61-7A") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "%x61-7A"))))
Theorem:
(defthm uri-cst-digit-conc-matching (implies (uri-cst-list-list-conc-matchp cstss "%x30-39") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "%x30-39"))))
Theorem:
(defthm uri-cst-hexdig-conc1-matching (implies (uri-cst-list-list-conc-matchp cstss "digit") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "digit"))))
Theorem:
(defthm uri-cst-hexdig-conc2-matching (implies (uri-cst-list-list-conc-matchp cstss "\"A\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"A\""))))
Theorem:
(defthm uri-cst-hexdig-conc3-matching (implies (uri-cst-list-list-conc-matchp cstss "\"B\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"B\""))))
Theorem:
(defthm uri-cst-hexdig-conc4-matching (implies (uri-cst-list-list-conc-matchp cstss "\"C\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"C\""))))
Theorem:
(defthm uri-cst-hexdig-conc5-matching (implies (uri-cst-list-list-conc-matchp cstss "\"D\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"D\""))))
Theorem:
(defthm uri-cst-hexdig-conc6-matching (implies (uri-cst-list-list-conc-matchp cstss "\"E\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"E\""))))
Theorem:
(defthm uri-cst-hexdig-conc7-matching (implies (uri-cst-list-list-conc-matchp cstss "\"F\"") (and (equal (len cstss) 1) (uri-cst-list-rep-matchp (nth 0 cstss) "\"F\""))))
Theorem:
(defthm uri-cst-hier-part-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "path-absolute") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-absolute"))))
Theorem:
(defthm uri-cst-hier-part-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "path-rootless") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-rootless"))))
Theorem:
(defthm uri-cst-hier-part-conc4-rep-matching (implies (uri-cst-list-rep-matchp csts "path-empty") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-empty"))))
Theorem:
(defthm uri-cst-uri-reference-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "uri") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "uri"))))
Theorem:
(defthm uri-cst-uri-reference-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "relative-ref") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "relative-ref"))))
Theorem:
(defthm uri-cst-relative-part-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "path-absolute") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-absolute"))))
Theorem:
(defthm uri-cst-relative-part-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "path-noscheme") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-noscheme"))))
Theorem:
(defthm uri-cst-relative-part-conc4-rep-matching (implies (uri-cst-list-rep-matchp csts "path-empty") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-empty"))))
Theorem:
(defthm uri-cst-host-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "ip-literal") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "ip-literal"))))
Theorem:
(defthm uri-cst-host-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "ipv4address") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "ipv4address"))))
Theorem:
(defthm uri-cst-host-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "reg-name") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "reg-name"))))
Theorem:
(defthm uri-cst-ls32-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "( h16 \":\" h16 )") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "( h16 \":\" h16 )"))))
Theorem:
(defthm uri-cst-ls32-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "ipv4address") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "ipv4address"))))
Theorem:
(defthm uri-cst-dec-octet-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "digit") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "digit"))))
Theorem:
(defthm uri-cst-path-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "path-abempty") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-abempty"))))
Theorem:
(defthm uri-cst-path-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "path-absolute") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-absolute"))))
Theorem:
(defthm uri-cst-path-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "path-noscheme") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-noscheme"))))
Theorem:
(defthm uri-cst-path-conc4-rep-matching (implies (uri-cst-list-rep-matchp csts "path-rootless") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-rootless"))))
Theorem:
(defthm uri-cst-path-conc5-rep-matching (implies (uri-cst-list-rep-matchp csts "path-empty") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "path-empty"))))
Theorem:
(defthm uri-cst-pchar-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "unreserved") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "unreserved"))))
Theorem:
(defthm uri-cst-pchar-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "pct-encoded") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "pct-encoded"))))
Theorem:
(defthm uri-cst-pchar-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "sub-delims") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "sub-delims"))))
Theorem:
(defthm uri-cst-pchar-conc4-rep-matching (implies (uri-cst-list-rep-matchp csts "\":\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\":\""))))
Theorem:
(defthm uri-cst-pchar-conc5-rep-matching (implies (uri-cst-list-rep-matchp csts "\"@\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"@\""))))
Theorem:
(defthm uri-cst-unreserved-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "alpha") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "alpha"))))
Theorem:
(defthm uri-cst-unreserved-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "digit") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "digit"))))
Theorem:
(defthm uri-cst-unreserved-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "\"-\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"-\""))))
Theorem:
(defthm uri-cst-unreserved-conc4-rep-matching (implies (uri-cst-list-rep-matchp csts "\".\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\".\""))))
Theorem:
(defthm uri-cst-unreserved-conc5-rep-matching (implies (uri-cst-list-rep-matchp csts "\"_\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"_\""))))
Theorem:
(defthm uri-cst-unreserved-conc6-rep-matching (implies (uri-cst-list-rep-matchp csts "\"~\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"~\""))))
Theorem:
(defthm uri-cst-reserved-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "gen-delims") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "gen-delims"))))
Theorem:
(defthm uri-cst-reserved-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "sub-delims") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "sub-delims"))))
Theorem:
(defthm uri-cst-gen-delims-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "\":\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\":\""))))
Theorem:
(defthm uri-cst-gen-delims-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "\"/\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"/\""))))
Theorem:
(defthm uri-cst-gen-delims-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "\"?\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"?\""))))
Theorem:
(defthm uri-cst-gen-delims-conc4-rep-matching (implies (uri-cst-list-rep-matchp csts "\"#\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"#\""))))
Theorem:
(defthm uri-cst-gen-delims-conc5-rep-matching (implies (uri-cst-list-rep-matchp csts "\"[\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"[\""))))
Theorem:
(defthm uri-cst-gen-delims-conc6-rep-matching (implies (uri-cst-list-rep-matchp csts "\"]\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"]\""))))
Theorem:
(defthm uri-cst-gen-delims-conc7-rep-matching (implies (uri-cst-list-rep-matchp csts "\"@\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"@\""))))
Theorem:
(defthm uri-cst-sub-delims-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "\"!\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"!\""))))
Theorem:
(defthm uri-cst-sub-delims-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "\"$\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"$\""))))
Theorem:
(defthm uri-cst-sub-delims-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "\"&\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"&\""))))
Theorem:
(defthm uri-cst-sub-delims-conc4-rep-matching (implies (uri-cst-list-rep-matchp csts "\"'\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"'\""))))
Theorem:
(defthm uri-cst-sub-delims-conc5-rep-matching (implies (uri-cst-list-rep-matchp csts "\"(\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"(\""))))
Theorem:
(defthm uri-cst-sub-delims-conc6-rep-matching (implies (uri-cst-list-rep-matchp csts "\")\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\")\""))))
Theorem:
(defthm uri-cst-sub-delims-conc7-rep-matching (implies (uri-cst-list-rep-matchp csts "\"*\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"*\""))))
Theorem:
(defthm uri-cst-sub-delims-conc8-rep-matching (implies (uri-cst-list-rep-matchp csts "\"+\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"+\""))))
Theorem:
(defthm uri-cst-sub-delims-conc9-rep-matching (implies (uri-cst-list-rep-matchp csts "\",\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\",\""))))
Theorem:
(defthm uri-cst-sub-delims-conc10-rep-matching (implies (uri-cst-list-rep-matchp csts "\";\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\";\""))))
Theorem:
(defthm uri-cst-sub-delims-conc11-rep-matching (implies (uri-cst-list-rep-matchp csts "\"=\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"=\""))))
Theorem:
(defthm uri-cst-alpha-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "%x41-5A") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "%x41-5A"))))
Theorem:
(defthm uri-cst-alpha-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "%x61-7A") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "%x61-7A"))))
Theorem:
(defthm uri-cst-digit-conc-rep-matching (implies (uri-cst-list-rep-matchp csts "%x30-39") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "%x30-39"))))
Theorem:
(defthm uri-cst-hexdig-conc1-rep-matching (implies (uri-cst-list-rep-matchp csts "digit") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "digit"))))
Theorem:
(defthm uri-cst-hexdig-conc2-rep-matching (implies (uri-cst-list-rep-matchp csts "\"A\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"A\""))))
Theorem:
(defthm uri-cst-hexdig-conc3-rep-matching (implies (uri-cst-list-rep-matchp csts "\"B\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"B\""))))
Theorem:
(defthm uri-cst-hexdig-conc4-rep-matching (implies (uri-cst-list-rep-matchp csts "\"C\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"C\""))))
Theorem:
(defthm uri-cst-hexdig-conc5-rep-matching (implies (uri-cst-list-rep-matchp csts "\"D\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"D\""))))
Theorem:
(defthm uri-cst-hexdig-conc6-rep-matching (implies (uri-cst-list-rep-matchp csts "\"E\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"E\""))))
Theorem:
(defthm uri-cst-hexdig-conc7-rep-matching (implies (uri-cst-list-rep-matchp csts "\"F\"") (and (equal (len csts) 1) (uri-cst-matchp (nth 0 csts) "\"F\""))))
Theorem:
(defthm uri-cst-uri-reference-conc-equivs (implies (uri-cst-matchp cst "uri-reference") (and (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "uri") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "uri"))) (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "relative-ref") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "relative-ref"))))))
Theorem:
(defthm uri-cst-host-conc-equivs (implies (uri-cst-matchp cst "host") (and (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "ip-literal") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "ip-literal"))) (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "ipv4address") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "ipv4address"))) (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "reg-name") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "reg-name"))))))
Theorem:
(defthm uri-cst-path-conc-equivs (implies (uri-cst-matchp cst "path") (and (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-abempty") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-abempty"))) (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-absolute") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-absolute"))) (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-noscheme") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-noscheme"))) (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-rootless") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-rootless"))) (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-empty") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-empty"))))))
Theorem:
(defthm uri-cst-reserved-conc-equivs (implies (uri-cst-matchp cst "reserved") (and (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "gen-delims") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "gen-delims"))) (iff (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "sub-delims") (equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "sub-delims"))))))
Function:
(defun uri-cst-uri-reference-conc? (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "uri-reference"))) (let ((__function__ 'uri-cst-uri-reference-conc?)) (declare (ignorable __function__)) (cond ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "uri")) 1) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "relative-ref")) 2) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-uri-cst-uri-reference-conc? (b* ((number (uri-cst-uri-reference-conc? cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc?-possibilities (b* ((number (uri-cst-uri-reference-conc? cst))) (or (equal number 1) (equal number 2))) :rule-classes ((:forward-chaining :trigger-terms ((uri-cst-uri-reference-conc? cst)))))
Theorem:
(defthm uri-cst-uri-reference-conc?-of-tree-fix-cst (equal (uri-cst-uri-reference-conc? (tree-fix cst)) (uri-cst-uri-reference-conc? cst)))
Theorem:
(defthm uri-cst-uri-reference-conc?-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-uri-reference-conc? cst) (uri-cst-uri-reference-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-uri-reference-conc?-1-iff-match-conc (implies (uri-cst-matchp cst "uri-reference") (iff (equal (uri-cst-uri-reference-conc? cst) 1) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "uri"))))
Theorem:
(defthm uri-cst-uri-reference-conc?-2-iff-match-conc (implies (uri-cst-matchp cst "uri-reference") (iff (equal (uri-cst-uri-reference-conc? cst) 2) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "relative-ref"))))
Function:
(defun uri-cst-host-conc? (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "host"))) (let ((__function__ 'uri-cst-host-conc?)) (declare (ignorable __function__)) (cond ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "ip-literal")) 1) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "ipv4address")) 2) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "reg-name")) 3) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-uri-cst-host-conc? (b* ((number (uri-cst-host-conc? cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc?-possibilities (b* ((number (uri-cst-host-conc? cst))) (or (equal number 1) (equal number 2) (equal number 3))) :rule-classes ((:forward-chaining :trigger-terms ((uri-cst-host-conc? cst)))))
Theorem:
(defthm uri-cst-host-conc?-of-tree-fix-cst (equal (uri-cst-host-conc? (tree-fix cst)) (uri-cst-host-conc? cst)))
Theorem:
(defthm uri-cst-host-conc?-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc? cst) (uri-cst-host-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-host-conc?-1-iff-match-conc (implies (uri-cst-matchp cst "host") (iff (equal (uri-cst-host-conc? cst) 1) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "ip-literal"))))
Theorem:
(defthm uri-cst-host-conc?-2-iff-match-conc (implies (uri-cst-matchp cst "host") (iff (equal (uri-cst-host-conc? cst) 2) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "ipv4address"))))
Theorem:
(defthm uri-cst-host-conc?-3-iff-match-conc (implies (uri-cst-matchp cst "host") (iff (equal (uri-cst-host-conc? cst) 3) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "reg-name"))))
Function:
(defun uri-cst-path-conc? (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "path"))) (let ((__function__ 'uri-cst-path-conc?)) (declare (ignorable __function__)) (cond ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-abempty")) 1) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-absolute")) 2) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-noscheme")) 3) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-rootless")) 4) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "path-empty")) 5) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-uri-cst-path-conc? (b* ((number (uri-cst-path-conc? cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc?-possibilities (b* ((number (uri-cst-path-conc? cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4) (equal number 5))) :rule-classes ((:forward-chaining :trigger-terms ((uri-cst-path-conc? cst)))))
Theorem:
(defthm uri-cst-path-conc?-of-tree-fix-cst (equal (uri-cst-path-conc? (tree-fix cst)) (uri-cst-path-conc? cst)))
Theorem:
(defthm uri-cst-path-conc?-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc? cst) (uri-cst-path-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-path-conc?-1-iff-match-conc (implies (uri-cst-matchp cst "path") (iff (equal (uri-cst-path-conc? cst) 1) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-abempty"))))
Theorem:
(defthm uri-cst-path-conc?-2-iff-match-conc (implies (uri-cst-matchp cst "path") (iff (equal (uri-cst-path-conc? cst) 2) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-absolute"))))
Theorem:
(defthm uri-cst-path-conc?-3-iff-match-conc (implies (uri-cst-matchp cst "path") (iff (equal (uri-cst-path-conc? cst) 3) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-noscheme"))))
Theorem:
(defthm uri-cst-path-conc?-4-iff-match-conc (implies (uri-cst-matchp cst "path") (iff (equal (uri-cst-path-conc? cst) 4) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-rootless"))))
Theorem:
(defthm uri-cst-path-conc?-5-iff-match-conc (implies (uri-cst-matchp cst "path") (iff (equal (uri-cst-path-conc? cst) 5) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "path-empty"))))
Function:
(defun uri-cst-reserved-conc? (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "reserved"))) (let ((__function__ 'uri-cst-reserved-conc?)) (declare (ignorable __function__)) (cond ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "gen-delims")) 1) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "sub-delims")) 2) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-uri-cst-reserved-conc? (b* ((number (uri-cst-reserved-conc? cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc?-possibilities (b* ((number (uri-cst-reserved-conc? cst))) (or (equal number 1) (equal number 2))) :rule-classes ((:forward-chaining :trigger-terms ((uri-cst-reserved-conc? cst)))))
Theorem:
(defthm uri-cst-reserved-conc?-of-tree-fix-cst (equal (uri-cst-reserved-conc? (tree-fix cst)) (uri-cst-reserved-conc? cst)))
Theorem:
(defthm uri-cst-reserved-conc?-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-reserved-conc? cst) (uri-cst-reserved-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm uri-cst-reserved-conc?-1-iff-match-conc (implies (uri-cst-matchp cst "reserved") (iff (equal (uri-cst-reserved-conc? cst) 1) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "gen-delims"))))
Theorem:
(defthm uri-cst-reserved-conc?-2-iff-match-conc (implies (uri-cst-matchp cst "reserved") (iff (equal (uri-cst-reserved-conc? cst) 2) (uri-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "sub-delims"))))
Function:
(defun uri-cst-uri-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "uri"))) (let ((__function__ 'uri-cst-uri-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-uri-conc (b* ((cstss (uri-cst-uri-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-conc-match (implies (uri-cst-matchp cst "uri") (b* ((cstss (uri-cst-uri-conc cst))) (uri-cst-list-list-conc-matchp cstss "scheme \":\" hier-part [ \"?\" query ] [ \"#\" fragment ]"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-conc-of-tree-fix-cst (equal (uri-cst-uri-conc (tree-fix cst)) (uri-cst-uri-conc cst)))
Theorem:
(defthm uri-cst-uri-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-uri-conc cst) (uri-cst-uri-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-uri-reference-conc1 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 1)))) (let ((__function__ 'uri-cst-uri-reference-conc1)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-uri-reference-conc1 (b* ((cstss (uri-cst-uri-reference-conc1 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc1-match (implies (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 1)) (b* ((cstss (uri-cst-uri-reference-conc1 cst))) (uri-cst-list-list-conc-matchp cstss "uri"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc1-of-tree-fix-cst (equal (uri-cst-uri-reference-conc1 (tree-fix cst)) (uri-cst-uri-reference-conc1 cst)))
Theorem:
(defthm uri-cst-uri-reference-conc1-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-uri-reference-conc1 cst) (uri-cst-uri-reference-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-uri-reference-conc2 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 2)))) (let ((__function__ 'uri-cst-uri-reference-conc2)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-uri-reference-conc2 (b* ((cstss (uri-cst-uri-reference-conc2 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc2-match (implies (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 2)) (b* ((cstss (uri-cst-uri-reference-conc2 cst))) (uri-cst-list-list-conc-matchp cstss "relative-ref"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc2-of-tree-fix-cst (equal (uri-cst-uri-reference-conc2 (tree-fix cst)) (uri-cst-uri-reference-conc2 cst)))
Theorem:
(defthm uri-cst-uri-reference-conc2-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-uri-reference-conc2 cst) (uri-cst-uri-reference-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-absolute-uri-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "absolute-uri"))) (let ((__function__ 'uri-cst-absolute-uri-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-absolute-uri-conc (b* ((cstss (uri-cst-absolute-uri-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-absolute-uri-conc-match (implies (uri-cst-matchp cst "absolute-uri") (b* ((cstss (uri-cst-absolute-uri-conc cst))) (uri-cst-list-list-conc-matchp cstss "scheme \":\" hier-part [ \"?\" query ]"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-absolute-uri-conc-of-tree-fix-cst (equal (uri-cst-absolute-uri-conc (tree-fix cst)) (uri-cst-absolute-uri-conc cst)))
Theorem:
(defthm uri-cst-absolute-uri-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-absolute-uri-conc cst) (uri-cst-absolute-uri-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-relative-ref-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "relative-ref"))) (let ((__function__ 'uri-cst-relative-ref-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-relative-ref-conc (b* ((cstss (uri-cst-relative-ref-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-relative-ref-conc-match (implies (uri-cst-matchp cst "relative-ref") (b* ((cstss (uri-cst-relative-ref-conc cst))) (uri-cst-list-list-conc-matchp cstss "relative-part [ \"?\" query ] [ \"#\" fragment ]"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-relative-ref-conc-of-tree-fix-cst (equal (uri-cst-relative-ref-conc (tree-fix cst)) (uri-cst-relative-ref-conc cst)))
Theorem:
(defthm uri-cst-relative-ref-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-relative-ref-conc cst) (uri-cst-relative-ref-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-scheme-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "scheme"))) (let ((__function__ 'uri-cst-scheme-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-scheme-conc (b* ((cstss (uri-cst-scheme-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-scheme-conc-match (implies (uri-cst-matchp cst "scheme") (b* ((cstss (uri-cst-scheme-conc cst))) (uri-cst-list-list-conc-matchp cstss "alpha *( alpha / digit / \"+\" / \"-\" / \".\" )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-scheme-conc-of-tree-fix-cst (equal (uri-cst-scheme-conc (tree-fix cst)) (uri-cst-scheme-conc cst)))
Theorem:
(defthm uri-cst-scheme-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-scheme-conc cst) (uri-cst-scheme-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-authority-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "authority"))) (let ((__function__ 'uri-cst-authority-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-authority-conc (b* ((cstss (uri-cst-authority-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-authority-conc-match (implies (uri-cst-matchp cst "authority") (b* ((cstss (uri-cst-authority-conc cst))) (uri-cst-list-list-conc-matchp cstss "[ userinfo \"@\" ] host [ \":\" port ]"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-authority-conc-of-tree-fix-cst (equal (uri-cst-authority-conc (tree-fix cst)) (uri-cst-authority-conc cst)))
Theorem:
(defthm uri-cst-authority-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-authority-conc cst) (uri-cst-authority-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-userinfo-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "userinfo"))) (let ((__function__ 'uri-cst-userinfo-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-userinfo-conc (b* ((cstss (uri-cst-userinfo-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-userinfo-conc-match (implies (uri-cst-matchp cst "userinfo") (b* ((cstss (uri-cst-userinfo-conc cst))) (uri-cst-list-list-conc-matchp cstss "*( unreserved / pct-encoded / sub-delims / \":\" )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-userinfo-conc-of-tree-fix-cst (equal (uri-cst-userinfo-conc (tree-fix cst)) (uri-cst-userinfo-conc cst)))
Theorem:
(defthm uri-cst-userinfo-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-userinfo-conc cst) (uri-cst-userinfo-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc1 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 1)))) (let ((__function__ 'uri-cst-host-conc1)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-host-conc1 (b* ((cstss (uri-cst-host-conc1 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc1-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 1)) (b* ((cstss (uri-cst-host-conc1 cst))) (uri-cst-list-list-conc-matchp cstss "ip-literal"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc1-of-tree-fix-cst (equal (uri-cst-host-conc1 (tree-fix cst)) (uri-cst-host-conc1 cst)))
Theorem:
(defthm uri-cst-host-conc1-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc1 cst) (uri-cst-host-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc2 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 2)))) (let ((__function__ 'uri-cst-host-conc2)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-host-conc2 (b* ((cstss (uri-cst-host-conc2 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc2-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 2)) (b* ((cstss (uri-cst-host-conc2 cst))) (uri-cst-list-list-conc-matchp cstss "ipv4address"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc2-of-tree-fix-cst (equal (uri-cst-host-conc2 (tree-fix cst)) (uri-cst-host-conc2 cst)))
Theorem:
(defthm uri-cst-host-conc2-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc2 cst) (uri-cst-host-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc3 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 3)))) (let ((__function__ 'uri-cst-host-conc3)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-host-conc3 (b* ((cstss (uri-cst-host-conc3 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc3-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 3)) (b* ((cstss (uri-cst-host-conc3 cst))) (uri-cst-list-list-conc-matchp cstss "reg-name"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc3-of-tree-fix-cst (equal (uri-cst-host-conc3 (tree-fix cst)) (uri-cst-host-conc3 cst)))
Theorem:
(defthm uri-cst-host-conc3-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc3 cst) (uri-cst-host-conc3 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-port-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "port"))) (let ((__function__ 'uri-cst-port-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-port-conc (b* ((cstss (uri-cst-port-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-port-conc-match (implies (uri-cst-matchp cst "port") (b* ((cstss (uri-cst-port-conc cst))) (uri-cst-list-list-conc-matchp cstss "*digit"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-port-conc-of-tree-fix-cst (equal (uri-cst-port-conc (tree-fix cst)) (uri-cst-port-conc cst)))
Theorem:
(defthm uri-cst-port-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-port-conc cst) (uri-cst-port-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-ip-literal-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "ip-literal"))) (let ((__function__ 'uri-cst-ip-literal-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-ip-literal-conc (b* ((cstss (uri-cst-ip-literal-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-ip-literal-conc-match (implies (uri-cst-matchp cst "ip-literal") (b* ((cstss (uri-cst-ip-literal-conc cst))) (uri-cst-list-list-conc-matchp cstss "\"[\" ( ipv6address / ipvfuture ) \"]\""))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-ip-literal-conc-of-tree-fix-cst (equal (uri-cst-ip-literal-conc (tree-fix cst)) (uri-cst-ip-literal-conc cst)))
Theorem:
(defthm uri-cst-ip-literal-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-ip-literal-conc cst) (uri-cst-ip-literal-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-ipvfuture-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "ipvfuture"))) (let ((__function__ 'uri-cst-ipvfuture-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-ipvfuture-conc (b* ((cstss (uri-cst-ipvfuture-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-ipvfuture-conc-match (implies (uri-cst-matchp cst "ipvfuture") (b* ((cstss (uri-cst-ipvfuture-conc cst))) (uri-cst-list-list-conc-matchp cstss "\"v\" 1*hexdig \".\" 1*( unreserved / sub-delims / \":\" )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-ipvfuture-conc-of-tree-fix-cst (equal (uri-cst-ipvfuture-conc (tree-fix cst)) (uri-cst-ipvfuture-conc cst)))
Theorem:
(defthm uri-cst-ipvfuture-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-ipvfuture-conc cst) (uri-cst-ipvfuture-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-h16-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "h16"))) (let ((__function__ 'uri-cst-h16-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-h16-conc (b* ((cstss (uri-cst-h16-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-h16-conc-match (implies (uri-cst-matchp cst "h16") (b* ((cstss (uri-cst-h16-conc cst))) (uri-cst-list-list-conc-matchp cstss "1*4hexdig"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-h16-conc-of-tree-fix-cst (equal (uri-cst-h16-conc (tree-fix cst)) (uri-cst-h16-conc cst)))
Theorem:
(defthm uri-cst-h16-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-h16-conc cst) (uri-cst-h16-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-ipv4address-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "ipv4address"))) (let ((__function__ 'uri-cst-ipv4address-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-ipv4address-conc (b* ((cstss (uri-cst-ipv4address-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-ipv4address-conc-match (implies (uri-cst-matchp cst "ipv4address") (b* ((cstss (uri-cst-ipv4address-conc cst))) (uri-cst-list-list-conc-matchp cstss "dec-octet \".\" dec-octet \".\" dec-octet \".\" dec-octet"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-ipv4address-conc-of-tree-fix-cst (equal (uri-cst-ipv4address-conc (tree-fix cst)) (uri-cst-ipv4address-conc cst)))
Theorem:
(defthm uri-cst-ipv4address-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-ipv4address-conc cst) (uri-cst-ipv4address-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-reg-name-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "reg-name"))) (let ((__function__ 'uri-cst-reg-name-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-reg-name-conc (b* ((cstss (uri-cst-reg-name-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reg-name-conc-match (implies (uri-cst-matchp cst "reg-name") (b* ((cstss (uri-cst-reg-name-conc cst))) (uri-cst-list-list-conc-matchp cstss "*( unreserved / pct-encoded / sub-delims )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reg-name-conc-of-tree-fix-cst (equal (uri-cst-reg-name-conc (tree-fix cst)) (uri-cst-reg-name-conc cst)))
Theorem:
(defthm uri-cst-reg-name-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-reg-name-conc cst) (uri-cst-reg-name-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc1 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 1)))) (let ((__function__ 'uri-cst-path-conc1)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-conc1 (b* ((cstss (uri-cst-path-conc1 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc1-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 1)) (b* ((cstss (uri-cst-path-conc1 cst))) (uri-cst-list-list-conc-matchp cstss "path-abempty"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc1-of-tree-fix-cst (equal (uri-cst-path-conc1 (tree-fix cst)) (uri-cst-path-conc1 cst)))
Theorem:
(defthm uri-cst-path-conc1-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc1 cst) (uri-cst-path-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc2 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 2)))) (let ((__function__ 'uri-cst-path-conc2)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-conc2 (b* ((cstss (uri-cst-path-conc2 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc2-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 2)) (b* ((cstss (uri-cst-path-conc2 cst))) (uri-cst-list-list-conc-matchp cstss "path-absolute"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc2-of-tree-fix-cst (equal (uri-cst-path-conc2 (tree-fix cst)) (uri-cst-path-conc2 cst)))
Theorem:
(defthm uri-cst-path-conc2-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc2 cst) (uri-cst-path-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc3 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 3)))) (let ((__function__ 'uri-cst-path-conc3)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-conc3 (b* ((cstss (uri-cst-path-conc3 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc3-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 3)) (b* ((cstss (uri-cst-path-conc3 cst))) (uri-cst-list-list-conc-matchp cstss "path-noscheme"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc3-of-tree-fix-cst (equal (uri-cst-path-conc3 (tree-fix cst)) (uri-cst-path-conc3 cst)))
Theorem:
(defthm uri-cst-path-conc3-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc3 cst) (uri-cst-path-conc3 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc4 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 4)))) (let ((__function__ 'uri-cst-path-conc4)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-conc4 (b* ((cstss (uri-cst-path-conc4 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc4-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 4)) (b* ((cstss (uri-cst-path-conc4 cst))) (uri-cst-list-list-conc-matchp cstss "path-rootless"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc4-of-tree-fix-cst (equal (uri-cst-path-conc4 (tree-fix cst)) (uri-cst-path-conc4 cst)))
Theorem:
(defthm uri-cst-path-conc4-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc4 cst) (uri-cst-path-conc4 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc5 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 5)))) (let ((__function__ 'uri-cst-path-conc5)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-conc5 (b* ((cstss (uri-cst-path-conc5 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc5-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 5)) (b* ((cstss (uri-cst-path-conc5 cst))) (uri-cst-list-list-conc-matchp cstss "path-empty"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc5-of-tree-fix-cst (equal (uri-cst-path-conc5 (tree-fix cst)) (uri-cst-path-conc5 cst)))
Theorem:
(defthm uri-cst-path-conc5-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc5 cst) (uri-cst-path-conc5 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-abempty-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "path-abempty"))) (let ((__function__ 'uri-cst-path-abempty-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-abempty-conc (b* ((cstss (uri-cst-path-abempty-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-abempty-conc-match (implies (uri-cst-matchp cst "path-abempty") (b* ((cstss (uri-cst-path-abempty-conc cst))) (uri-cst-list-list-conc-matchp cstss "*( \"/\" segment )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-abempty-conc-of-tree-fix-cst (equal (uri-cst-path-abempty-conc (tree-fix cst)) (uri-cst-path-abempty-conc cst)))
Theorem:
(defthm uri-cst-path-abempty-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-abempty-conc cst) (uri-cst-path-abempty-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-absolute-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "path-absolute"))) (let ((__function__ 'uri-cst-path-absolute-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-absolute-conc (b* ((cstss (uri-cst-path-absolute-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-absolute-conc-match (implies (uri-cst-matchp cst "path-absolute") (b* ((cstss (uri-cst-path-absolute-conc cst))) (uri-cst-list-list-conc-matchp cstss "\"/\" [ segment-nz *( \"/\" segment ) ]"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-absolute-conc-of-tree-fix-cst (equal (uri-cst-path-absolute-conc (tree-fix cst)) (uri-cst-path-absolute-conc cst)))
Theorem:
(defthm uri-cst-path-absolute-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-absolute-conc cst) (uri-cst-path-absolute-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-noscheme-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "path-noscheme"))) (let ((__function__ 'uri-cst-path-noscheme-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-noscheme-conc (b* ((cstss (uri-cst-path-noscheme-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-noscheme-conc-match (implies (uri-cst-matchp cst "path-noscheme") (b* ((cstss (uri-cst-path-noscheme-conc cst))) (uri-cst-list-list-conc-matchp cstss "segment-nz-nc *( \"/\" segment )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-noscheme-conc-of-tree-fix-cst (equal (uri-cst-path-noscheme-conc (tree-fix cst)) (uri-cst-path-noscheme-conc cst)))
Theorem:
(defthm uri-cst-path-noscheme-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-noscheme-conc cst) (uri-cst-path-noscheme-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-rootless-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "path-rootless"))) (let ((__function__ 'uri-cst-path-rootless-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-rootless-conc (b* ((cstss (uri-cst-path-rootless-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-rootless-conc-match (implies (uri-cst-matchp cst "path-rootless") (b* ((cstss (uri-cst-path-rootless-conc cst))) (uri-cst-list-list-conc-matchp cstss "segment-nz *( \"/\" segment )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-rootless-conc-of-tree-fix-cst (equal (uri-cst-path-rootless-conc (tree-fix cst)) (uri-cst-path-rootless-conc cst)))
Theorem:
(defthm uri-cst-path-rootless-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-rootless-conc cst) (uri-cst-path-rootless-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-empty-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "path-empty"))) (let ((__function__ 'uri-cst-path-empty-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-path-empty-conc (b* ((cstss (uri-cst-path-empty-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-empty-conc-match (implies (uri-cst-matchp cst "path-empty") (b* ((cstss (uri-cst-path-empty-conc cst))) (uri-cst-list-list-conc-matchp cstss "0<pchar>"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-empty-conc-of-tree-fix-cst (equal (uri-cst-path-empty-conc (tree-fix cst)) (uri-cst-path-empty-conc cst)))
Theorem:
(defthm uri-cst-path-empty-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-empty-conc cst) (uri-cst-path-empty-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-segment-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "segment"))) (let ((__function__ 'uri-cst-segment-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-segment-conc (b* ((cstss (uri-cst-segment-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-segment-conc-match (implies (uri-cst-matchp cst "segment") (b* ((cstss (uri-cst-segment-conc cst))) (uri-cst-list-list-conc-matchp cstss "*pchar"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-segment-conc-of-tree-fix-cst (equal (uri-cst-segment-conc (tree-fix cst)) (uri-cst-segment-conc cst)))
Theorem:
(defthm uri-cst-segment-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-segment-conc cst) (uri-cst-segment-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-segment-nz-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "segment-nz"))) (let ((__function__ 'uri-cst-segment-nz-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-segment-nz-conc (b* ((cstss (uri-cst-segment-nz-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-segment-nz-conc-match (implies (uri-cst-matchp cst "segment-nz") (b* ((cstss (uri-cst-segment-nz-conc cst))) (uri-cst-list-list-conc-matchp cstss "1*pchar"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-segment-nz-conc-of-tree-fix-cst (equal (uri-cst-segment-nz-conc (tree-fix cst)) (uri-cst-segment-nz-conc cst)))
Theorem:
(defthm uri-cst-segment-nz-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-segment-nz-conc cst) (uri-cst-segment-nz-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-segment-nz-nc-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "segment-nz-nc"))) (let ((__function__ 'uri-cst-segment-nz-nc-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-segment-nz-nc-conc (b* ((cstss (uri-cst-segment-nz-nc-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-segment-nz-nc-conc-match (implies (uri-cst-matchp cst "segment-nz-nc") (b* ((cstss (uri-cst-segment-nz-nc-conc cst))) (uri-cst-list-list-conc-matchp cstss "1*( unreserved / pct-encoded / sub-delims / \"@\" )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-segment-nz-nc-conc-of-tree-fix-cst (equal (uri-cst-segment-nz-nc-conc (tree-fix cst)) (uri-cst-segment-nz-nc-conc cst)))
Theorem:
(defthm uri-cst-segment-nz-nc-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-segment-nz-nc-conc cst) (uri-cst-segment-nz-nc-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-query-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "query"))) (let ((__function__ 'uri-cst-query-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-query-conc (b* ((cstss (uri-cst-query-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-query-conc-match (implies (uri-cst-matchp cst "query") (b* ((cstss (uri-cst-query-conc cst))) (uri-cst-list-list-conc-matchp cstss "*( pchar / \"/\" / \"?\" )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-query-conc-of-tree-fix-cst (equal (uri-cst-query-conc (tree-fix cst)) (uri-cst-query-conc cst)))
Theorem:
(defthm uri-cst-query-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-query-conc cst) (uri-cst-query-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-fragment-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "fragment"))) (let ((__function__ 'uri-cst-fragment-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-fragment-conc (b* ((cstss (uri-cst-fragment-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-fragment-conc-match (implies (uri-cst-matchp cst "fragment") (b* ((cstss (uri-cst-fragment-conc cst))) (uri-cst-list-list-conc-matchp cstss "*( pchar / \"/\" / \"?\" )"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-fragment-conc-of-tree-fix-cst (equal (uri-cst-fragment-conc (tree-fix cst)) (uri-cst-fragment-conc cst)))
Theorem:
(defthm uri-cst-fragment-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-fragment-conc cst) (uri-cst-fragment-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-pct-encoded-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "pct-encoded"))) (let ((__function__ 'uri-cst-pct-encoded-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-pct-encoded-conc (b* ((cstss (uri-cst-pct-encoded-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-pct-encoded-conc-match (implies (uri-cst-matchp cst "pct-encoded") (b* ((cstss (uri-cst-pct-encoded-conc cst))) (uri-cst-list-list-conc-matchp cstss "\"%\" hexdig hexdig"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-pct-encoded-conc-of-tree-fix-cst (equal (uri-cst-pct-encoded-conc (tree-fix cst)) (uri-cst-pct-encoded-conc cst)))
Theorem:
(defthm uri-cst-pct-encoded-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-pct-encoded-conc cst) (uri-cst-pct-encoded-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-reserved-conc1 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 1)))) (let ((__function__ 'uri-cst-reserved-conc1)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-reserved-conc1 (b* ((cstss (uri-cst-reserved-conc1 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc1-match (implies (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 1)) (b* ((cstss (uri-cst-reserved-conc1 cst))) (uri-cst-list-list-conc-matchp cstss "gen-delims"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc1-of-tree-fix-cst (equal (uri-cst-reserved-conc1 (tree-fix cst)) (uri-cst-reserved-conc1 cst)))
Theorem:
(defthm uri-cst-reserved-conc1-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-reserved-conc1 cst) (uri-cst-reserved-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-reserved-conc2 (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 2)))) (let ((__function__ 'uri-cst-reserved-conc2)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-reserved-conc2 (b* ((cstss (uri-cst-reserved-conc2 cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc2-match (implies (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 2)) (b* ((cstss (uri-cst-reserved-conc2 cst))) (uri-cst-list-list-conc-matchp cstss "sub-delims"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc2-of-tree-fix-cst (equal (uri-cst-reserved-conc2 (tree-fix cst)) (uri-cst-reserved-conc2 cst)))
Theorem:
(defthm uri-cst-reserved-conc2-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-reserved-conc2 cst) (uri-cst-reserved-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-digit-conc (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "digit"))) (let ((__function__ 'uri-cst-digit-conc)) (declare (ignorable __function__)) (tree-nonleaf->branches cst)))
Theorem:
(defthm tree-list-listp-of-uri-cst-digit-conc (b* ((cstss (uri-cst-digit-conc cst))) (tree-list-listp cstss)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-digit-conc-match (implies (uri-cst-matchp cst "digit") (b* ((cstss (uri-cst-digit-conc cst))) (uri-cst-list-list-conc-matchp cstss "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-digit-conc-of-tree-fix-cst (equal (uri-cst-digit-conc (tree-fix cst)) (uri-cst-digit-conc cst)))
Theorem:
(defthm uri-cst-digit-conc-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-digit-conc cst) (uri-cst-digit-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-uri-reference-conc1-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 1)))) (let ((__function__ 'uri-cst-uri-reference-conc1-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-uri-reference-conc1 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-uri-reference-conc1-rep (b* ((csts (uri-cst-uri-reference-conc1-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc1-rep-match (implies (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 1)) (b* ((csts (uri-cst-uri-reference-conc1-rep cst))) (uri-cst-list-rep-matchp csts "uri"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc1-rep-of-tree-fix-cst (equal (uri-cst-uri-reference-conc1-rep (tree-fix cst)) (uri-cst-uri-reference-conc1-rep cst)))
Theorem:
(defthm uri-cst-uri-reference-conc1-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-uri-reference-conc1-rep cst) (uri-cst-uri-reference-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-uri-reference-conc2-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 2)))) (let ((__function__ 'uri-cst-uri-reference-conc2-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-uri-reference-conc2 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-uri-reference-conc2-rep (b* ((csts (uri-cst-uri-reference-conc2-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc2-rep-match (implies (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 2)) (b* ((csts (uri-cst-uri-reference-conc2-rep cst))) (uri-cst-list-rep-matchp csts "relative-ref"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc2-rep-of-tree-fix-cst (equal (uri-cst-uri-reference-conc2-rep (tree-fix cst)) (uri-cst-uri-reference-conc2-rep cst)))
Theorem:
(defthm uri-cst-uri-reference-conc2-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-uri-reference-conc2-rep cst) (uri-cst-uri-reference-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc1-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 1)))) (let ((__function__ 'uri-cst-host-conc1-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-host-conc1 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-host-conc1-rep (b* ((csts (uri-cst-host-conc1-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc1-rep-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 1)) (b* ((csts (uri-cst-host-conc1-rep cst))) (uri-cst-list-rep-matchp csts "ip-literal"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc1-rep-of-tree-fix-cst (equal (uri-cst-host-conc1-rep (tree-fix cst)) (uri-cst-host-conc1-rep cst)))
Theorem:
(defthm uri-cst-host-conc1-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc1-rep cst) (uri-cst-host-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc2-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 2)))) (let ((__function__ 'uri-cst-host-conc2-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-host-conc2 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-host-conc2-rep (b* ((csts (uri-cst-host-conc2-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc2-rep-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 2)) (b* ((csts (uri-cst-host-conc2-rep cst))) (uri-cst-list-rep-matchp csts "ipv4address"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc2-rep-of-tree-fix-cst (equal (uri-cst-host-conc2-rep (tree-fix cst)) (uri-cst-host-conc2-rep cst)))
Theorem:
(defthm uri-cst-host-conc2-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc2-rep cst) (uri-cst-host-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc3-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 3)))) (let ((__function__ 'uri-cst-host-conc3-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-host-conc3 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-host-conc3-rep (b* ((csts (uri-cst-host-conc3-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc3-rep-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 3)) (b* ((csts (uri-cst-host-conc3-rep cst))) (uri-cst-list-rep-matchp csts "reg-name"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc3-rep-of-tree-fix-cst (equal (uri-cst-host-conc3-rep (tree-fix cst)) (uri-cst-host-conc3-rep cst)))
Theorem:
(defthm uri-cst-host-conc3-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc3-rep cst) (uri-cst-host-conc3-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc1-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 1)))) (let ((__function__ 'uri-cst-path-conc1-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-path-conc1 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-path-conc1-rep (b* ((csts (uri-cst-path-conc1-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc1-rep-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 1)) (b* ((csts (uri-cst-path-conc1-rep cst))) (uri-cst-list-rep-matchp csts "path-abempty"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc1-rep-of-tree-fix-cst (equal (uri-cst-path-conc1-rep (tree-fix cst)) (uri-cst-path-conc1-rep cst)))
Theorem:
(defthm uri-cst-path-conc1-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc1-rep cst) (uri-cst-path-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc2-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 2)))) (let ((__function__ 'uri-cst-path-conc2-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-path-conc2 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-path-conc2-rep (b* ((csts (uri-cst-path-conc2-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc2-rep-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 2)) (b* ((csts (uri-cst-path-conc2-rep cst))) (uri-cst-list-rep-matchp csts "path-absolute"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc2-rep-of-tree-fix-cst (equal (uri-cst-path-conc2-rep (tree-fix cst)) (uri-cst-path-conc2-rep cst)))
Theorem:
(defthm uri-cst-path-conc2-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc2-rep cst) (uri-cst-path-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc3-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 3)))) (let ((__function__ 'uri-cst-path-conc3-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-path-conc3 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-path-conc3-rep (b* ((csts (uri-cst-path-conc3-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc3-rep-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 3)) (b* ((csts (uri-cst-path-conc3-rep cst))) (uri-cst-list-rep-matchp csts "path-noscheme"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc3-rep-of-tree-fix-cst (equal (uri-cst-path-conc3-rep (tree-fix cst)) (uri-cst-path-conc3-rep cst)))
Theorem:
(defthm uri-cst-path-conc3-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc3-rep cst) (uri-cst-path-conc3-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc4-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 4)))) (let ((__function__ 'uri-cst-path-conc4-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-path-conc4 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-path-conc4-rep (b* ((csts (uri-cst-path-conc4-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc4-rep-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 4)) (b* ((csts (uri-cst-path-conc4-rep cst))) (uri-cst-list-rep-matchp csts "path-rootless"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc4-rep-of-tree-fix-cst (equal (uri-cst-path-conc4-rep (tree-fix cst)) (uri-cst-path-conc4-rep cst)))
Theorem:
(defthm uri-cst-path-conc4-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc4-rep cst) (uri-cst-path-conc4-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc5-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 5)))) (let ((__function__ 'uri-cst-path-conc5-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-path-conc5 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-path-conc5-rep (b* ((csts (uri-cst-path-conc5-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc5-rep-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 5)) (b* ((csts (uri-cst-path-conc5-rep cst))) (uri-cst-list-rep-matchp csts "path-empty"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc5-rep-of-tree-fix-cst (equal (uri-cst-path-conc5-rep (tree-fix cst)) (uri-cst-path-conc5-rep cst)))
Theorem:
(defthm uri-cst-path-conc5-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc5-rep cst) (uri-cst-path-conc5-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-reserved-conc1-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 1)))) (let ((__function__ 'uri-cst-reserved-conc1-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-reserved-conc1 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-reserved-conc1-rep (b* ((csts (uri-cst-reserved-conc1-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc1-rep-match (implies (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 1)) (b* ((csts (uri-cst-reserved-conc1-rep cst))) (uri-cst-list-rep-matchp csts "gen-delims"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc1-rep-of-tree-fix-cst (equal (uri-cst-reserved-conc1-rep (tree-fix cst)) (uri-cst-reserved-conc1-rep cst)))
Theorem:
(defthm uri-cst-reserved-conc1-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-reserved-conc1-rep cst) (uri-cst-reserved-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-reserved-conc2-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 2)))) (let ((__function__ 'uri-cst-reserved-conc2-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-reserved-conc2 cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-reserved-conc2-rep (b* ((csts (uri-cst-reserved-conc2-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc2-rep-match (implies (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 2)) (b* ((csts (uri-cst-reserved-conc2-rep cst))) (uri-cst-list-rep-matchp csts "sub-delims"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc2-rep-of-tree-fix-cst (equal (uri-cst-reserved-conc2-rep (tree-fix cst)) (uri-cst-reserved-conc2-rep cst)))
Theorem:
(defthm uri-cst-reserved-conc2-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-reserved-conc2-rep cst) (uri-cst-reserved-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-digit-conc-rep (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "digit"))) (let ((__function__ 'uri-cst-digit-conc-rep)) (declare (ignorable __function__)) (tree-list-fix (nth 0 (uri-cst-digit-conc cst)))))
Theorem:
(defthm tree-listp-of-uri-cst-digit-conc-rep (b* ((csts (uri-cst-digit-conc-rep cst))) (tree-listp csts)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-digit-conc-rep-match (implies (uri-cst-matchp cst "digit") (b* ((csts (uri-cst-digit-conc-rep cst))) (uri-cst-list-rep-matchp csts "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-digit-conc-rep-of-tree-fix-cst (equal (uri-cst-digit-conc-rep (tree-fix cst)) (uri-cst-digit-conc-rep cst)))
Theorem:
(defthm uri-cst-digit-conc-rep-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-digit-conc-rep cst) (uri-cst-digit-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-uri-reference-conc1-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 1)))) (let ((__function__ 'uri-cst-uri-reference-conc1-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-uri-reference-conc1-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-uri-reference-conc1-rep-elem (b* ((cst1 (uri-cst-uri-reference-conc1-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc1-rep-elem-match (implies (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 1)) (b* ((cst1 (uri-cst-uri-reference-conc1-rep-elem cst))) (uri-cst-matchp cst1 "uri"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc1-rep-elem-of-tree-fix-cst (equal (uri-cst-uri-reference-conc1-rep-elem (tree-fix cst)) (uri-cst-uri-reference-conc1-rep-elem cst)))
Theorem:
(defthm uri-cst-uri-reference-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-uri-reference-conc1-rep-elem cst) (uri-cst-uri-reference-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-uri-reference-conc2-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 2)))) (let ((__function__ 'uri-cst-uri-reference-conc2-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-uri-reference-conc2-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-uri-reference-conc2-rep-elem (b* ((cst1 (uri-cst-uri-reference-conc2-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc2-rep-elem-match (implies (and (uri-cst-matchp cst "uri-reference") (equal (uri-cst-uri-reference-conc? cst) 2)) (b* ((cst1 (uri-cst-uri-reference-conc2-rep-elem cst))) (uri-cst-matchp cst1 "relative-ref"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-uri-reference-conc2-rep-elem-of-tree-fix-cst (equal (uri-cst-uri-reference-conc2-rep-elem (tree-fix cst)) (uri-cst-uri-reference-conc2-rep-elem cst)))
Theorem:
(defthm uri-cst-uri-reference-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-uri-reference-conc2-rep-elem cst) (uri-cst-uri-reference-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc1-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 1)))) (let ((__function__ 'uri-cst-host-conc1-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-host-conc1-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-host-conc1-rep-elem (b* ((cst1 (uri-cst-host-conc1-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc1-rep-elem-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 1)) (b* ((cst1 (uri-cst-host-conc1-rep-elem cst))) (uri-cst-matchp cst1 "ip-literal"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc1-rep-elem-of-tree-fix-cst (equal (uri-cst-host-conc1-rep-elem (tree-fix cst)) (uri-cst-host-conc1-rep-elem cst)))
Theorem:
(defthm uri-cst-host-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc1-rep-elem cst) (uri-cst-host-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc2-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 2)))) (let ((__function__ 'uri-cst-host-conc2-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-host-conc2-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-host-conc2-rep-elem (b* ((cst1 (uri-cst-host-conc2-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc2-rep-elem-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 2)) (b* ((cst1 (uri-cst-host-conc2-rep-elem cst))) (uri-cst-matchp cst1 "ipv4address"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc2-rep-elem-of-tree-fix-cst (equal (uri-cst-host-conc2-rep-elem (tree-fix cst)) (uri-cst-host-conc2-rep-elem cst)))
Theorem:
(defthm uri-cst-host-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc2-rep-elem cst) (uri-cst-host-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-host-conc3-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 3)))) (let ((__function__ 'uri-cst-host-conc3-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-host-conc3-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-host-conc3-rep-elem (b* ((cst1 (uri-cst-host-conc3-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc3-rep-elem-match (implies (and (uri-cst-matchp cst "host") (equal (uri-cst-host-conc? cst) 3)) (b* ((cst1 (uri-cst-host-conc3-rep-elem cst))) (uri-cst-matchp cst1 "reg-name"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-host-conc3-rep-elem-of-tree-fix-cst (equal (uri-cst-host-conc3-rep-elem (tree-fix cst)) (uri-cst-host-conc3-rep-elem cst)))
Theorem:
(defthm uri-cst-host-conc3-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-host-conc3-rep-elem cst) (uri-cst-host-conc3-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc1-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 1)))) (let ((__function__ 'uri-cst-path-conc1-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-path-conc1-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-path-conc1-rep-elem (b* ((cst1 (uri-cst-path-conc1-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc1-rep-elem-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 1)) (b* ((cst1 (uri-cst-path-conc1-rep-elem cst))) (uri-cst-matchp cst1 "path-abempty"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc1-rep-elem-of-tree-fix-cst (equal (uri-cst-path-conc1-rep-elem (tree-fix cst)) (uri-cst-path-conc1-rep-elem cst)))
Theorem:
(defthm uri-cst-path-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc1-rep-elem cst) (uri-cst-path-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc2-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 2)))) (let ((__function__ 'uri-cst-path-conc2-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-path-conc2-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-path-conc2-rep-elem (b* ((cst1 (uri-cst-path-conc2-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc2-rep-elem-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 2)) (b* ((cst1 (uri-cst-path-conc2-rep-elem cst))) (uri-cst-matchp cst1 "path-absolute"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc2-rep-elem-of-tree-fix-cst (equal (uri-cst-path-conc2-rep-elem (tree-fix cst)) (uri-cst-path-conc2-rep-elem cst)))
Theorem:
(defthm uri-cst-path-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc2-rep-elem cst) (uri-cst-path-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc3-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 3)))) (let ((__function__ 'uri-cst-path-conc3-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-path-conc3-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-path-conc3-rep-elem (b* ((cst1 (uri-cst-path-conc3-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc3-rep-elem-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 3)) (b* ((cst1 (uri-cst-path-conc3-rep-elem cst))) (uri-cst-matchp cst1 "path-noscheme"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc3-rep-elem-of-tree-fix-cst (equal (uri-cst-path-conc3-rep-elem (tree-fix cst)) (uri-cst-path-conc3-rep-elem cst)))
Theorem:
(defthm uri-cst-path-conc3-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc3-rep-elem cst) (uri-cst-path-conc3-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc4-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 4)))) (let ((__function__ 'uri-cst-path-conc4-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-path-conc4-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-path-conc4-rep-elem (b* ((cst1 (uri-cst-path-conc4-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc4-rep-elem-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 4)) (b* ((cst1 (uri-cst-path-conc4-rep-elem cst))) (uri-cst-matchp cst1 "path-rootless"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc4-rep-elem-of-tree-fix-cst (equal (uri-cst-path-conc4-rep-elem (tree-fix cst)) (uri-cst-path-conc4-rep-elem cst)))
Theorem:
(defthm uri-cst-path-conc4-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc4-rep-elem cst) (uri-cst-path-conc4-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-path-conc5-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 5)))) (let ((__function__ 'uri-cst-path-conc5-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-path-conc5-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-path-conc5-rep-elem (b* ((cst1 (uri-cst-path-conc5-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc5-rep-elem-match (implies (and (uri-cst-matchp cst "path") (equal (uri-cst-path-conc? cst) 5)) (b* ((cst1 (uri-cst-path-conc5-rep-elem cst))) (uri-cst-matchp cst1 "path-empty"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-path-conc5-rep-elem-of-tree-fix-cst (equal (uri-cst-path-conc5-rep-elem (tree-fix cst)) (uri-cst-path-conc5-rep-elem cst)))
Theorem:
(defthm uri-cst-path-conc5-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-path-conc5-rep-elem cst) (uri-cst-path-conc5-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-reserved-conc1-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 1)))) (let ((__function__ 'uri-cst-reserved-conc1-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-reserved-conc1-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-reserved-conc1-rep-elem (b* ((cst1 (uri-cst-reserved-conc1-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc1-rep-elem-match (implies (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 1)) (b* ((cst1 (uri-cst-reserved-conc1-rep-elem cst))) (uri-cst-matchp cst1 "gen-delims"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc1-rep-elem-of-tree-fix-cst (equal (uri-cst-reserved-conc1-rep-elem (tree-fix cst)) (uri-cst-reserved-conc1-rep-elem cst)))
Theorem:
(defthm uri-cst-reserved-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-reserved-conc1-rep-elem cst) (uri-cst-reserved-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-reserved-conc2-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 2)))) (let ((__function__ 'uri-cst-reserved-conc2-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-reserved-conc2-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-reserved-conc2-rep-elem (b* ((cst1 (uri-cst-reserved-conc2-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc2-rep-elem-match (implies (and (uri-cst-matchp cst "reserved") (equal (uri-cst-reserved-conc? cst) 2)) (b* ((cst1 (uri-cst-reserved-conc2-rep-elem cst))) (uri-cst-matchp cst1 "sub-delims"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-reserved-conc2-rep-elem-of-tree-fix-cst (equal (uri-cst-reserved-conc2-rep-elem (tree-fix cst)) (uri-cst-reserved-conc2-rep-elem cst)))
Theorem:
(defthm uri-cst-reserved-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-reserved-conc2-rep-elem cst) (uri-cst-reserved-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun uri-cst-digit-conc-rep-elem (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (uri-cst-matchp cst "digit"))) (let ((__function__ 'uri-cst-digit-conc-rep-elem)) (declare (ignorable __function__)) (tree-fix (nth 0 (uri-cst-digit-conc-rep cst)))))
Theorem:
(defthm treep-of-uri-cst-digit-conc-rep-elem (b* ((cst1 (uri-cst-digit-conc-rep-elem cst))) (treep cst1)) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-digit-conc-rep-elem-match (implies (uri-cst-matchp cst "digit") (b* ((cst1 (uri-cst-digit-conc-rep-elem cst))) (uri-cst-matchp cst1 "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm uri-cst-digit-conc-rep-elem-of-tree-fix-cst (equal (uri-cst-digit-conc-rep-elem (tree-fix cst)) (uri-cst-digit-conc-rep-elem cst)))
Theorem:
(defthm uri-cst-digit-conc-rep-elem-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (uri-cst-digit-conc-rep-elem cst) (uri-cst-digit-conc-rep-elem cst-equiv))) :rule-classes :congruence)