|
|
|---|
|
|
|
|---|
Tree operations specialized to *grammar*.
Function:
(defun cst-matchp$ (abnf::tree abnf::elem) (declare (xargs :guard (and (abnf::treep abnf::tree) (abnf::elementp abnf::elem)))) (let ((__function__ 'cst-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-terminatedp abnf::tree) (abnf::tree-match-element-p abnf::tree abnf::elem *grammar*))))
Theorem:
(defthm booleanp-of-cst-matchp$ (b* ((abnf::yes/no (cst-matchp$ abnf::tree abnf::elem))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-matchp$-of-tree-fix-tree (equal (cst-matchp$ (abnf::tree-fix abnf::tree) abnf::elem) (cst-matchp$ abnf::tree abnf::elem)))
Theorem:
(defthm cst-matchp$-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv abnf::tree tree-equiv) (equal (cst-matchp$ abnf::tree abnf::elem) (cst-matchp$ tree-equiv abnf::elem))) :rule-classes :congruence)
Theorem:
(defthm cst-matchp$-of-element-fix-elem (equal (cst-matchp$ abnf::tree (abnf::element-fix abnf::elem)) (cst-matchp$ abnf::tree abnf::elem)))
Theorem:
(defthm cst-matchp$-element-equiv-congruence-on-elem (implies (abnf::element-equiv abnf::elem elem-equiv) (equal (cst-matchp$ abnf::tree abnf::elem) (cst-matchp$ abnf::tree elem-equiv))) :rule-classes :congruence)
Function:
(defun cst-list-elem-matchp$ (abnf::trees abnf::elem) (declare (xargs :guard (and (abnf::tree-listp abnf::trees) (abnf::elementp abnf::elem)))) (let ((__function__ 'cst-list-elem-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-list-terminatedp abnf::trees) (abnf::tree-list-match-element-p abnf::trees abnf::elem *grammar*))))
Theorem:
(defthm booleanp-of-cst-list-elem-matchp$ (b* ((abnf::yes/no (cst-list-elem-matchp$ abnf::trees abnf::elem))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-list-elem-matchp$-of-tree-list-fix-trees (equal (cst-list-elem-matchp$ (abnf::tree-list-fix abnf::trees) abnf::elem) (cst-list-elem-matchp$ abnf::trees abnf::elem)))
Theorem:
(defthm cst-list-elem-matchp$-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv abnf::trees trees-equiv) (equal (cst-list-elem-matchp$ abnf::trees abnf::elem) (cst-list-elem-matchp$ trees-equiv abnf::elem))) :rule-classes :congruence)
Theorem:
(defthm cst-list-elem-matchp$-of-element-fix-elem (equal (cst-list-elem-matchp$ abnf::trees (abnf::element-fix abnf::elem)) (cst-list-elem-matchp$ abnf::trees abnf::elem)))
Theorem:
(defthm cst-list-elem-matchp$-element-equiv-congruence-on-elem (implies (abnf::element-equiv abnf::elem elem-equiv) (equal (cst-list-elem-matchp$ abnf::trees abnf::elem) (cst-list-elem-matchp$ abnf::trees elem-equiv))) :rule-classes :congruence)
Function:
(defun cst-list-rep-matchp$ (abnf::trees abnf::rep) (declare (xargs :guard (and (abnf::tree-listp abnf::trees) (abnf::repetitionp abnf::rep)))) (let ((__function__ 'cst-list-rep-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-list-terminatedp abnf::trees) (abnf::tree-list-match-repetition-p abnf::trees abnf::rep *grammar*))))
Theorem:
(defthm booleanp-of-cst-list-rep-matchp$ (b* ((abnf::yes/no (cst-list-rep-matchp$ abnf::trees abnf::rep))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-list-rep-matchp$-of-tree-list-fix-trees (equal (cst-list-rep-matchp$ (abnf::tree-list-fix abnf::trees) abnf::rep) (cst-list-rep-matchp$ abnf::trees abnf::rep)))
Theorem:
(defthm cst-list-rep-matchp$-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv abnf::trees trees-equiv) (equal (cst-list-rep-matchp$ abnf::trees abnf::rep) (cst-list-rep-matchp$ trees-equiv abnf::rep))) :rule-classes :congruence)
Theorem:
(defthm cst-list-rep-matchp$-of-repetition-fix-rep (equal (cst-list-rep-matchp$ abnf::trees (abnf::repetition-fix abnf::rep)) (cst-list-rep-matchp$ abnf::trees abnf::rep)))
Theorem:
(defthm cst-list-rep-matchp$-repetition-equiv-congruence-on-rep (implies (abnf::repetition-equiv abnf::rep rep-equiv) (equal (cst-list-rep-matchp$ abnf::trees abnf::rep) (cst-list-rep-matchp$ abnf::trees rep-equiv))) :rule-classes :congruence)
Function:
(defun cst-list-list-conc-matchp$ (abnf::treess abnf::conc) (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess) (abnf::concatenationp abnf::conc)))) (let ((__function__ 'cst-list-list-conc-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-list-list-terminatedp abnf::treess) (abnf::tree-list-list-match-concatenation-p abnf::treess abnf::conc *grammar*))))
Theorem:
(defthm booleanp-of-cst-list-list-conc-matchp$ (b* ((abnf::yes/no (cst-list-list-conc-matchp$ abnf::treess abnf::conc))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-list-list-conc-matchp$-of-tree-list-list-fix-treess (equal (cst-list-list-conc-matchp$ (abnf::tree-list-list-fix abnf::treess) abnf::conc) (cst-list-list-conc-matchp$ abnf::treess abnf::conc)))
Theorem:
(defthm cst-list-list-conc-matchp$-tree-list-list-equiv-congruence-on-treess (implies (abnf::tree-list-list-equiv abnf::treess treess-equiv) (equal (cst-list-list-conc-matchp$ abnf::treess abnf::conc) (cst-list-list-conc-matchp$ treess-equiv abnf::conc))) :rule-classes :congruence)
Theorem:
(defthm cst-list-list-conc-matchp$-of-concatenation-fix-conc (equal (cst-list-list-conc-matchp$ abnf::treess (abnf::concatenation-fix abnf::conc)) (cst-list-list-conc-matchp$ abnf::treess abnf::conc)))
Theorem:
(defthm cst-list-list-conc-matchp$-concatenation-equiv-congruence-on-conc (implies (abnf::concatenation-equiv abnf::conc conc-equiv) (equal (cst-list-list-conc-matchp$ abnf::treess abnf::conc) (cst-list-list-conc-matchp$ abnf::treess conc-equiv))) :rule-classes :congruence)
Function:
(defun cst-list-list-alt-matchp$ (abnf::treess abnf::alt) (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess) (abnf::alternationp abnf::alt)))) (let ((__function__ 'cst-list-list-alt-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-list-list-terminatedp abnf::treess) (abnf::tree-list-list-match-alternation-p abnf::treess abnf::alt *grammar*))))
Theorem:
(defthm booleanp-of-cst-list-list-alt-matchp$ (b* ((abnf::yes/no (cst-list-list-alt-matchp$ abnf::treess abnf::alt))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-list-list-alt-matchp$-of-tree-list-list-fix-treess (equal (cst-list-list-alt-matchp$ (abnf::tree-list-list-fix abnf::treess) abnf::alt) (cst-list-list-alt-matchp$ abnf::treess abnf::alt)))
Theorem:
(defthm cst-list-list-alt-matchp$-tree-list-list-equiv-congruence-on-treess (implies (abnf::tree-list-list-equiv abnf::treess treess-equiv) (equal (cst-list-list-alt-matchp$ abnf::treess abnf::alt) (cst-list-list-alt-matchp$ treess-equiv abnf::alt))) :rule-classes :congruence)
Theorem:
(defthm cst-list-list-alt-matchp$-of-alternation-fix-alt (equal (cst-list-list-alt-matchp$ abnf::treess (abnf::alternation-fix abnf::alt)) (cst-list-list-alt-matchp$ abnf::treess abnf::alt)))
Theorem:
(defthm cst-list-list-alt-matchp$-alternation-equiv-congruence-on-alt (implies (abnf::alternation-equiv abnf::alt alt-equiv) (equal (cst-list-list-alt-matchp$ abnf::treess abnf::alt) (cst-list-list-alt-matchp$ abnf::treess alt-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x30-39-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x30-39"))) (let ((__function__ 'cst-%x30-39-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x30-39-nat (b* ((nat (cst-%x30-39-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x30-39-nat-of-tree-fix-cst (equal (cst-%x30-39-nat (abnf::tree-fix abnf::cst)) (cst-%x30-39-nat abnf::cst)))
Theorem:
(defthm cst-%x30-39-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x30-39-nat abnf::cst) (cst-%x30-39-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x41-5a-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x41-5A"))) (let ((__function__ 'cst-%x41-5a-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x41-5a-nat (b* ((nat (cst-%x41-5a-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x41-5a-nat-of-tree-fix-cst (equal (cst-%x41-5a-nat (abnf::tree-fix abnf::cst)) (cst-%x41-5a-nat abnf::cst)))
Theorem:
(defthm cst-%x41-5a-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x41-5a-nat abnf::cst) (cst-%x41-5a-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x61-7a-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x61-7A"))) (let ((__function__ 'cst-%x61-7a-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x61-7a-nat (b* ((nat (cst-%x61-7a-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x61-7a-nat-of-tree-fix-cst (equal (cst-%x61-7a-nat (abnf::tree-fix abnf::cst)) (cst-%x61-7a-nat abnf::cst)))
Theorem:
(defthm cst-%x61-7a-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x61-7a-nat abnf::cst) (cst-%x61-7a-nat cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-%x30-39-nat-bounds (implies (cst-matchp abnf::cst "%x30-39") (and (<= 48 (cst-%x30-39-nat abnf::cst)) (<= (cst-%x30-39-nat abnf::cst) 57))) :rule-classes :linear)
Theorem:
(defthm cst-%x41-5a-nat-bounds (implies (cst-matchp abnf::cst "%x41-5A") (and (<= 65 (cst-%x41-5a-nat abnf::cst)) (<= (cst-%x41-5a-nat abnf::cst) 90))) :rule-classes :linear)
Theorem:
(defthm cst-%x61-7a-nat-bounds (implies (cst-matchp abnf::cst "%x61-7A") (and (<= 97 (cst-%x61-7a-nat abnf::cst)) (<= (cst-%x61-7a-nat abnf::cst) 122))) :rule-classes :linear)
Theorem:
(defthm |CST-"("-LEAFTERM| (implies (cst-matchp abnf::cst "\"(\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-")"-LEAFTERM| (implies (cst-matchp abnf::cst "\")\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"*"-LEAFTERM| (implies (cst-matchp abnf::cst "\"*\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"+"-LEAFTERM| (implies (cst-matchp abnf::cst "\"+\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-","-LEAFTERM| (implies (cst-matchp abnf::cst "\",\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"-"-LEAFTERM| (implies (cst-matchp abnf::cst "\"-\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-":="-LEAFTERM| (implies (cst-matchp abnf::cst "\":=\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"=="-LEAFTERM| (implies (cst-matchp abnf::cst "\"==\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"_"-LEAFTERM| (implies (cst-matchp abnf::cst "\"_\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"{"-LEAFTERM| (implies (cst-matchp abnf::cst "\"{\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"}"-LEAFTERM| (implies (cst-matchp abnf::cst "\"}\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm cst-line-feed-nonleaf (implies (cst-matchp abnf::cst "line-feed") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-carriage-return-nonleaf (implies (cst-matchp abnf::cst "carriage-return") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-space-nonleaf (implies (cst-matchp abnf::cst "space") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-line-terminator-nonleaf (implies (cst-matchp abnf::cst "line-terminator") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-whitespace-nonleaf (implies (cst-matchp abnf::cst "whitespace") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-uppercase-letter-nonleaf (implies (cst-matchp abnf::cst "uppercase-letter") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-lowercase-letter-nonleaf (implies (cst-matchp abnf::cst "lowercase-letter") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-letter-nonleaf (implies (cst-matchp abnf::cst "letter") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-digit-nonleaf (implies (cst-matchp abnf::cst "digit") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-numeral-nonleaf (implies (cst-matchp abnf::cst "numeral") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-identifier-nonleaf (implies (cst-matchp abnf::cst "identifier") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-operator-nonleaf (implies (cst-matchp abnf::cst "operator") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-separator-nonleaf (implies (cst-matchp abnf::cst "separator") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-token-nonleaf (implies (cst-matchp abnf::cst "token") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-lexeme-nonleaf (implies (cst-matchp abnf::cst "lexeme") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-primary-expression-nonleaf (implies (cst-matchp abnf::cst "primary-expression") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-unary-minus-expression-nonleaf (implies (cst-matchp abnf::cst "unary-minus-expression") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-multiplication-expression-nonleaf (implies (cst-matchp abnf::cst "multiplication-expression") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-additive-expression-nonleaf (implies (cst-matchp abnf::cst "additive-expression") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-expression-nonleaf (implies (cst-matchp abnf::cst "expression") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-equality-constraint-nonleaf (implies (cst-matchp abnf::cst "equality-constraint") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-relation-constraint-nonleaf (implies (cst-matchp abnf::cst "relation-constraint") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-constraint-nonleaf (implies (cst-matchp abnf::cst "constraint") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-definition-nonleaf (implies (cst-matchp abnf::cst "definition") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-system-nonleaf (implies (cst-matchp abnf::cst "system") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-line-feed-rulename (implies (cst-matchp abnf::cst "line-feed") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "line-feed"))))
Theorem:
(defthm cst-carriage-return-rulename (implies (cst-matchp abnf::cst "carriage-return") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "carriage-return"))))
Theorem:
(defthm cst-space-rulename (implies (cst-matchp abnf::cst "space") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "space"))))
Theorem:
(defthm cst-line-terminator-rulename (implies (cst-matchp abnf::cst "line-terminator") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "line-terminator"))))
Theorem:
(defthm cst-whitespace-rulename (implies (cst-matchp abnf::cst "whitespace") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "whitespace"))))
Theorem:
(defthm cst-uppercase-letter-rulename (implies (cst-matchp abnf::cst "uppercase-letter") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "uppercase-letter"))))
Theorem:
(defthm cst-lowercase-letter-rulename (implies (cst-matchp abnf::cst "lowercase-letter") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "lowercase-letter"))))
Theorem:
(defthm cst-letter-rulename (implies (cst-matchp abnf::cst "letter") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "letter"))))
Theorem:
(defthm cst-digit-rulename (implies (cst-matchp abnf::cst "digit") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "digit"))))
Theorem:
(defthm cst-numeral-rulename (implies (cst-matchp abnf::cst "numeral") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "numeral"))))
Theorem:
(defthm cst-identifier-rulename (implies (cst-matchp abnf::cst "identifier") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "identifier"))))
Theorem:
(defthm cst-operator-rulename (implies (cst-matchp abnf::cst "operator") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "operator"))))
Theorem:
(defthm cst-separator-rulename (implies (cst-matchp abnf::cst "separator") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "separator"))))
Theorem:
(defthm cst-token-rulename (implies (cst-matchp abnf::cst "token") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "token"))))
Theorem:
(defthm cst-lexeme-rulename (implies (cst-matchp abnf::cst "lexeme") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "lexeme"))))
Theorem:
(defthm cst-primary-expression-rulename (implies (cst-matchp abnf::cst "primary-expression") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "primary-expression"))))
Theorem:
(defthm cst-unary-minus-expression-rulename (implies (cst-matchp abnf::cst "unary-minus-expression") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "unary-minus-expression"))))
Theorem:
(defthm cst-multiplication-expression-rulename (implies (cst-matchp abnf::cst "multiplication-expression") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "multiplication-expression"))))
Theorem:
(defthm cst-additive-expression-rulename (implies (cst-matchp abnf::cst "additive-expression") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "additive-expression"))))
Theorem:
(defthm cst-expression-rulename (implies (cst-matchp abnf::cst "expression") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "expression"))))
Theorem:
(defthm cst-equality-constraint-rulename (implies (cst-matchp abnf::cst "equality-constraint") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "equality-constraint"))))
Theorem:
(defthm cst-relation-constraint-rulename (implies (cst-matchp abnf::cst "relation-constraint") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "relation-constraint"))))
Theorem:
(defthm cst-constraint-rulename (implies (cst-matchp abnf::cst "constraint") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "constraint"))))
Theorem:
(defthm cst-definition-rulename (implies (cst-matchp abnf::cst "definition") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "definition"))))
Theorem:
(defthm cst-system-rulename (implies (cst-matchp abnf::cst "system") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "system"))))
Theorem:
(defthm cst-line-feed-branches-match-alt (implies (cst-matchp abnf::cst "line-feed") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%xA")))
Theorem:
(defthm cst-carriage-return-branches-match-alt (implies (cst-matchp abnf::cst "carriage-return") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%xD")))
Theorem:
(defthm cst-space-branches-match-alt (implies (cst-matchp abnf::cst "space") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x20")))
Theorem:
(defthm cst-line-terminator-branches-match-alt (implies (cst-matchp abnf::cst "line-terminator") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "[ carriage-return ] line-feed")))
Theorem:
(defthm cst-whitespace-branches-match-alt (implies (cst-matchp abnf::cst "whitespace") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "space / line-terminator")))
Theorem:
(defthm cst-uppercase-letter-branches-match-alt (implies (cst-matchp abnf::cst "uppercase-letter") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x41-5A")))
Theorem:
(defthm cst-lowercase-letter-branches-match-alt (implies (cst-matchp abnf::cst "lowercase-letter") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x61-7A")))
Theorem:
(defthm cst-letter-branches-match-alt (implies (cst-matchp abnf::cst "letter") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "uppercase-letter / lowercase-letter")))
Theorem:
(defthm cst-digit-branches-match-alt (implies (cst-matchp abnf::cst "digit") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x30-39")))
Theorem:
(defthm cst-numeral-branches-match-alt (implies (cst-matchp abnf::cst "numeral") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "1*digit")))
Theorem:
(defthm cst-identifier-branches-match-alt (implies (cst-matchp abnf::cst "identifier") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "letter *( letter / digit / \"_\" )")))
Theorem:
(defthm cst-operator-branches-match-alt (implies (cst-matchp abnf::cst "operator") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"+\" / \"-\" / \"*\" / \":=\" / \"==\"")))
Theorem:
(defthm cst-separator-branches-match-alt (implies (cst-matchp abnf::cst "separator") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"(\" / \")\" / \"{\" / \"}\" / \",\"")))
Theorem:
(defthm cst-token-branches-match-alt (implies (cst-matchp abnf::cst "token") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier / numeral / operator / separator")))
Theorem:
(defthm cst-lexeme-branches-match-alt (implies (cst-matchp abnf::cst "lexeme") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "token / whitespace")))
Theorem:
(defthm cst-primary-expression-branches-match-alt (implies (cst-matchp abnf::cst "primary-expression") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier / numeral / \"(\" expression \")\"")))
Theorem:
(defthm cst-unary-minus-expression-branches-match-alt (implies (cst-matchp abnf::cst "unary-minus-expression") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "[ \"-\" ] primary-expression")))
Theorem:
(defthm cst-multiplication-expression-branches-match-alt (implies (cst-matchp abnf::cst "multiplication-expression") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "unary-minus-expression / multiplication-expression \"*\" unary-minus-expression")))
Theorem:
(defthm cst-additive-expression-branches-match-alt (implies (cst-matchp abnf::cst "additive-expression") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "multiplication-expression / additive-expression \"+\" multiplication-expression / additive-expression \"-\" multiplication-expression")))
Theorem:
(defthm cst-expression-branches-match-alt (implies (cst-matchp abnf::cst "expression") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "additive-expression")))
Theorem:
(defthm cst-equality-constraint-branches-match-alt (implies (cst-matchp abnf::cst "equality-constraint") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "expression \"==\" expression")))
Theorem:
(defthm cst-relation-constraint-branches-match-alt (implies (cst-matchp abnf::cst "relation-constraint") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier \"(\" [ expression *( \",\" expression ) ] \")\"")))
Theorem:
(defthm cst-constraint-branches-match-alt (implies (cst-matchp abnf::cst "constraint") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "equality-constraint / relation-constraint")))
Theorem:
(defthm cst-definition-branches-match-alt (implies (cst-matchp abnf::cst "definition") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier \"(\" [ identifier *( \",\" identifier ) ] \")\" \":=\" \"{\" [ constraint *( \",\" constraint ) ] \"}\"")))
Theorem:
(defthm cst-system-branches-match-alt (implies (cst-matchp abnf::cst "system") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "*definition *constraint")))
Theorem:
(defthm cst-line-feed-concs (implies (cst-list-list-alt-matchp abnf::cstss "%xA") (or (cst-list-list-conc-matchp abnf::cstss "%xA"))))
Theorem:
(defthm cst-carriage-return-concs (implies (cst-list-list-alt-matchp abnf::cstss "%xD") (or (cst-list-list-conc-matchp abnf::cstss "%xD"))))
Theorem:
(defthm cst-space-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x20") (or (cst-list-list-conc-matchp abnf::cstss "%x20"))))
Theorem:
(defthm cst-line-terminator-concs (implies (cst-list-list-alt-matchp abnf::cstss "[ carriage-return ] line-feed") (or (cst-list-list-conc-matchp abnf::cstss "[ carriage-return ] line-feed"))))
Theorem:
(defthm cst-whitespace-concs (implies (cst-list-list-alt-matchp abnf::cstss "space / line-terminator") (or (cst-list-list-conc-matchp abnf::cstss "space") (cst-list-list-conc-matchp abnf::cstss "line-terminator"))))
Theorem:
(defthm cst-uppercase-letter-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x41-5A") (or (cst-list-list-conc-matchp abnf::cstss "%x41-5A"))))
Theorem:
(defthm cst-lowercase-letter-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x61-7A") (or (cst-list-list-conc-matchp abnf::cstss "%x61-7A"))))
Theorem:
(defthm cst-letter-concs (implies (cst-list-list-alt-matchp abnf::cstss "uppercase-letter / lowercase-letter") (or (cst-list-list-conc-matchp abnf::cstss "uppercase-letter") (cst-list-list-conc-matchp abnf::cstss "lowercase-letter"))))
Theorem:
(defthm cst-digit-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x30-39") (or (cst-list-list-conc-matchp abnf::cstss "%x30-39"))))
Theorem:
(defthm cst-numeral-concs (implies (cst-list-list-alt-matchp abnf::cstss "1*digit") (or (cst-list-list-conc-matchp abnf::cstss "1*digit"))))
Theorem:
(defthm cst-identifier-concs (implies (cst-list-list-alt-matchp abnf::cstss "letter *( letter / digit / \"_\" )") (or (cst-list-list-conc-matchp abnf::cstss "letter *( letter / digit / \"_\" )"))))
Theorem:
(defthm cst-operator-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"+\" / \"-\" / \"*\" / \":=\" / \"==\"") (or (cst-list-list-conc-matchp abnf::cstss "\"+\"") (cst-list-list-conc-matchp abnf::cstss "\"-\"") (cst-list-list-conc-matchp abnf::cstss "\"*\"") (cst-list-list-conc-matchp abnf::cstss "\":=\"") (cst-list-list-conc-matchp abnf::cstss "\"==\""))))
Theorem:
(defthm cst-separator-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"(\" / \")\" / \"{\" / \"}\" / \",\"") (or (cst-list-list-conc-matchp abnf::cstss "\"(\"") (cst-list-list-conc-matchp abnf::cstss "\")\"") (cst-list-list-conc-matchp abnf::cstss "\"{\"") (cst-list-list-conc-matchp abnf::cstss "\"}\"") (cst-list-list-conc-matchp abnf::cstss "\",\""))))
Theorem:
(defthm cst-token-concs (implies (cst-list-list-alt-matchp abnf::cstss "identifier / numeral / operator / separator") (or (cst-list-list-conc-matchp abnf::cstss "identifier") (cst-list-list-conc-matchp abnf::cstss "numeral") (cst-list-list-conc-matchp abnf::cstss "operator") (cst-list-list-conc-matchp abnf::cstss "separator"))))
Theorem:
(defthm cst-lexeme-concs (implies (cst-list-list-alt-matchp abnf::cstss "token / whitespace") (or (cst-list-list-conc-matchp abnf::cstss "token") (cst-list-list-conc-matchp abnf::cstss "whitespace"))))
Theorem:
(defthm cst-primary-expression-concs (implies (cst-list-list-alt-matchp abnf::cstss "identifier / numeral / \"(\" expression \")\"") (or (cst-list-list-conc-matchp abnf::cstss "identifier") (cst-list-list-conc-matchp abnf::cstss "numeral") (cst-list-list-conc-matchp abnf::cstss "\"(\" expression \")\""))))
Theorem:
(defthm cst-unary-minus-expression-concs (implies (cst-list-list-alt-matchp abnf::cstss "[ \"-\" ] primary-expression") (or (cst-list-list-conc-matchp abnf::cstss "[ \"-\" ] primary-expression"))))
Theorem:
(defthm cst-multiplication-expression-concs (implies (cst-list-list-alt-matchp abnf::cstss "unary-minus-expression / multiplication-expression \"*\" unary-minus-expression") (or (cst-list-list-conc-matchp abnf::cstss "unary-minus-expression") (cst-list-list-conc-matchp abnf::cstss "multiplication-expression \"*\" unary-minus-expression"))))
Theorem:
(defthm cst-additive-expression-concs (implies (cst-list-list-alt-matchp abnf::cstss "multiplication-expression / additive-expression \"+\" multiplication-expression / additive-expression \"-\" multiplication-expression") (or (cst-list-list-conc-matchp abnf::cstss "multiplication-expression") (cst-list-list-conc-matchp abnf::cstss "additive-expression \"+\" multiplication-expression") (cst-list-list-conc-matchp abnf::cstss "additive-expression \"-\" multiplication-expression"))))
Theorem:
(defthm cst-expression-concs (implies (cst-list-list-alt-matchp abnf::cstss "additive-expression") (or (cst-list-list-conc-matchp abnf::cstss "additive-expression"))))
Theorem:
(defthm cst-equality-constraint-concs (implies (cst-list-list-alt-matchp abnf::cstss "expression \"==\" expression") (or (cst-list-list-conc-matchp abnf::cstss "expression \"==\" expression"))))
Theorem:
(defthm cst-relation-constraint-concs (implies (cst-list-list-alt-matchp abnf::cstss "identifier \"(\" [ expression *( \",\" expression ) ] \")\"") (or (cst-list-list-conc-matchp abnf::cstss "identifier \"(\" [ expression *( \",\" expression ) ] \")\""))))
Theorem:
(defthm cst-constraint-concs (implies (cst-list-list-alt-matchp abnf::cstss "equality-constraint / relation-constraint") (or (cst-list-list-conc-matchp abnf::cstss "equality-constraint") (cst-list-list-conc-matchp abnf::cstss "relation-constraint"))))
Theorem:
(defthm cst-definition-concs (implies (cst-list-list-alt-matchp abnf::cstss "identifier \"(\" [ identifier *( \",\" identifier ) ] \")\" \":=\" \"{\" [ constraint *( \",\" constraint ) ] \"}\"") (or (cst-list-list-conc-matchp abnf::cstss "identifier \"(\" [ identifier *( \",\" identifier ) ] \")\" \":=\" \"{\" [ constraint *( \",\" constraint ) ] \"}\""))))
Theorem:
(defthm cst-system-concs (implies (cst-list-list-alt-matchp abnf::cstss "*definition *constraint") (or (cst-list-list-conc-matchp abnf::cstss "*definition *constraint"))))
Theorem:
(defthm cst-line-feed-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xA") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xA"))))
Theorem:
(defthm cst-carriage-return-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xD") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xD"))))
Theorem:
(defthm cst-space-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x20") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x20"))))
Theorem:
(defthm cst-whitespace-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "space") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "space"))))
Theorem:
(defthm cst-whitespace-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "line-terminator") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "line-terminator"))))
Theorem:
(defthm cst-uppercase-letter-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x41-5A") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x41-5A"))))
Theorem:
(defthm cst-lowercase-letter-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x61-7A") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x61-7A"))))
Theorem:
(defthm cst-letter-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "uppercase-letter") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "uppercase-letter"))))
Theorem:
(defthm cst-letter-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "lowercase-letter") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "lowercase-letter"))))
Theorem:
(defthm cst-digit-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x30-39") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x30-39"))))
Theorem:
(defthm cst-numeral-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "1*digit") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "1*digit"))))
Theorem:
(defthm cst-operator-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"+\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"+\""))))
Theorem:
(defthm cst-operator-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"-\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"-\""))))
Theorem:
(defthm cst-operator-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"*\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"*\""))))
Theorem:
(defthm cst-operator-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "\":=\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\":=\""))))
Theorem:
(defthm cst-operator-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"==\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"==\""))))
Theorem:
(defthm cst-separator-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"(\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"(\""))))
Theorem:
(defthm cst-separator-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "\")\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\")\""))))
Theorem:
(defthm cst-separator-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"{\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"{\""))))
Theorem:
(defthm cst-separator-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"}\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"}\""))))
Theorem:
(defthm cst-separator-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "\",\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\",\""))))
Theorem:
(defthm cst-token-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "identifier") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "identifier"))))
Theorem:
(defthm cst-token-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "numeral") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "numeral"))))
Theorem:
(defthm cst-token-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "operator") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "operator"))))
Theorem:
(defthm cst-token-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "separator") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "separator"))))
Theorem:
(defthm cst-lexeme-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "token") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "token"))))
Theorem:
(defthm cst-lexeme-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "whitespace") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "whitespace"))))
Theorem:
(defthm cst-primary-expression-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "identifier") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "identifier"))))
Theorem:
(defthm cst-primary-expression-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "numeral") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "numeral"))))
Theorem:
(defthm cst-multiplication-expression-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "unary-minus-expression") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "unary-minus-expression"))))
Theorem:
(defthm cst-additive-expression-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "multiplication-expression") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "multiplication-expression"))))
Theorem:
(defthm cst-expression-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "additive-expression") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "additive-expression"))))
Theorem:
(defthm cst-constraint-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "equality-constraint") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "equality-constraint"))))
Theorem:
(defthm cst-constraint-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "relation-constraint") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "relation-constraint"))))
Theorem:
(defthm cst-line-feed-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xA") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xA"))))
Theorem:
(defthm cst-carriage-return-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xD") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xD"))))
Theorem:
(defthm cst-space-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x20") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x20"))))
Theorem:
(defthm cst-whitespace-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "space") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "space"))))
Theorem:
(defthm cst-whitespace-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "line-terminator") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "line-terminator"))))
Theorem:
(defthm cst-uppercase-letter-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x41-5A") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x41-5A"))))
Theorem:
(defthm cst-lowercase-letter-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x61-7A") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x61-7A"))))
Theorem:
(defthm cst-letter-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "uppercase-letter") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "uppercase-letter"))))
Theorem:
(defthm cst-letter-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "lowercase-letter") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "lowercase-letter"))))
Theorem:
(defthm cst-digit-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x30-39") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x30-39"))))
Theorem:
(defthm cst-operator-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"+\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"+\""))))
Theorem:
(defthm cst-operator-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"-\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"-\""))))
Theorem:
(defthm cst-operator-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"*\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"*\""))))
Theorem:
(defthm cst-operator-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "\":=\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\":=\""))))
Theorem:
(defthm cst-operator-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"==\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"==\""))))
Theorem:
(defthm cst-separator-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"(\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"(\""))))
Theorem:
(defthm cst-separator-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "\")\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\")\""))))
Theorem:
(defthm cst-separator-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"{\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"{\""))))
Theorem:
(defthm cst-separator-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"}\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"}\""))))
Theorem:
(defthm cst-separator-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "\",\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\",\""))))
Theorem:
(defthm cst-token-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "identifier") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "identifier"))))
Theorem:
(defthm cst-token-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "numeral") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "numeral"))))
Theorem:
(defthm cst-token-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "operator") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "operator"))))
Theorem:
(defthm cst-token-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "separator") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "separator"))))
Theorem:
(defthm cst-lexeme-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "token") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "token"))))
Theorem:
(defthm cst-lexeme-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "whitespace") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "whitespace"))))
Theorem:
(defthm cst-primary-expression-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "identifier") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "identifier"))))
Theorem:
(defthm cst-primary-expression-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "numeral") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "numeral"))))
Theorem:
(defthm cst-multiplication-expression-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "unary-minus-expression") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "unary-minus-expression"))))
Theorem:
(defthm cst-additive-expression-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "multiplication-expression") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "multiplication-expression"))))
Theorem:
(defthm cst-expression-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "additive-expression") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "additive-expression"))))
Theorem:
(defthm cst-constraint-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "equality-constraint") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "equality-constraint"))))
Theorem:
(defthm cst-constraint-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "relation-constraint") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "relation-constraint"))))
Theorem:
(defthm cst-whitespace-conc-equivs (implies (cst-matchp abnf::cst "whitespace") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "space") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "space"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "line-terminator") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "line-terminator"))))))
Theorem:
(defthm cst-letter-conc-equivs (implies (cst-matchp abnf::cst "letter") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "uppercase-letter") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "uppercase-letter"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "lowercase-letter") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "lowercase-letter"))))))
Theorem:
(defthm cst-token-conc-equivs (implies (cst-matchp abnf::cst "token") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "identifier"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "numeral") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "numeral"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "operator") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "operator"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "separator") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "separator"))))))
Theorem:
(defthm cst-lexeme-conc-equivs (implies (cst-matchp abnf::cst "lexeme") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "token") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "token"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "whitespace") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "whitespace"))))))
Theorem:
(defthm cst-constraint-conc-equivs (implies (cst-matchp abnf::cst "constraint") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "equality-constraint") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "equality-constraint"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "relation-constraint") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "relation-constraint"))))))
Function:
(defun cst-whitespace-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "whitespace"))) (let ((__function__ 'cst-whitespace-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "space")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "line-terminator")) 2) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-whitespace-conc? (b* ((number (cst-whitespace-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc?-possibilities (b* ((number (cst-whitespace-conc? abnf::cst))) (or (equal number 1) (equal number 2))) :rule-classes ((:forward-chaining :trigger-terms ((cst-whitespace-conc? abnf::cst)))))
Theorem:
(defthm cst-whitespace-conc?-of-tree-fix-cst (equal (cst-whitespace-conc? (abnf::tree-fix abnf::cst)) (cst-whitespace-conc? abnf::cst)))
Theorem:
(defthm cst-whitespace-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-whitespace-conc? abnf::cst) (cst-whitespace-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-whitespace-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "whitespace") (iff (equal (cst-whitespace-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "space"))))
Theorem:
(defthm cst-whitespace-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "whitespace") (iff (equal (cst-whitespace-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "line-terminator"))))
Function:
(defun cst-letter-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "letter"))) (let ((__function__ 'cst-letter-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "uppercase-letter")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "lowercase-letter")) 2) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-letter-conc? (b* ((number (cst-letter-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc?-possibilities (b* ((number (cst-letter-conc? abnf::cst))) (or (equal number 1) (equal number 2))) :rule-classes ((:forward-chaining :trigger-terms ((cst-letter-conc? abnf::cst)))))
Theorem:
(defthm cst-letter-conc?-of-tree-fix-cst (equal (cst-letter-conc? (abnf::tree-fix abnf::cst)) (cst-letter-conc? abnf::cst)))
Theorem:
(defthm cst-letter-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-letter-conc? abnf::cst) (cst-letter-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-letter-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "letter") (iff (equal (cst-letter-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "uppercase-letter"))))
Theorem:
(defthm cst-letter-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "letter") (iff (equal (cst-letter-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "lowercase-letter"))))
Function:
(defun cst-token-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "token"))) (let ((__function__ 'cst-token-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "identifier")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "numeral")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "operator")) 3) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "separator")) 4) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-token-conc? (b* ((number (cst-token-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc?-possibilities (b* ((number (cst-token-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4))) :rule-classes ((:forward-chaining :trigger-terms ((cst-token-conc? abnf::cst)))))
Theorem:
(defthm cst-token-conc?-of-tree-fix-cst (equal (cst-token-conc? (abnf::tree-fix abnf::cst)) (cst-token-conc? abnf::cst)))
Theorem:
(defthm cst-token-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc? abnf::cst) (cst-token-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-token-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "token") (iff (equal (cst-token-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier"))))
Theorem:
(defthm cst-token-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "token") (iff (equal (cst-token-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "numeral"))))
Theorem:
(defthm cst-token-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "token") (iff (equal (cst-token-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "operator"))))
Theorem:
(defthm cst-token-conc?-4-iff-match-conc (implies (cst-matchp abnf::cst "token") (iff (equal (cst-token-conc? abnf::cst) 4) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "separator"))))
Function:
(defun cst-lexeme-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lexeme"))) (let ((__function__ 'cst-lexeme-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "token")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "whitespace")) 2) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-lexeme-conc? (b* ((number (cst-lexeme-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc?-possibilities (b* ((number (cst-lexeme-conc? abnf::cst))) (or (equal number 1) (equal number 2))) :rule-classes ((:forward-chaining :trigger-terms ((cst-lexeme-conc? abnf::cst)))))
Theorem:
(defthm cst-lexeme-conc?-of-tree-fix-cst (equal (cst-lexeme-conc? (abnf::tree-fix abnf::cst)) (cst-lexeme-conc? abnf::cst)))
Theorem:
(defthm cst-lexeme-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc? abnf::cst) (cst-lexeme-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-lexeme-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "lexeme") (iff (equal (cst-lexeme-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "token"))))
Theorem:
(defthm cst-lexeme-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "lexeme") (iff (equal (cst-lexeme-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "whitespace"))))
Function:
(defun cst-constraint-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "constraint"))) (let ((__function__ 'cst-constraint-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "equality-constraint")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "relation-constraint")) 2) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-constraint-conc? (b* ((number (cst-constraint-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc?-possibilities (b* ((number (cst-constraint-conc? abnf::cst))) (or (equal number 1) (equal number 2))) :rule-classes ((:forward-chaining :trigger-terms ((cst-constraint-conc? abnf::cst)))))
Theorem:
(defthm cst-constraint-conc?-of-tree-fix-cst (equal (cst-constraint-conc? (abnf::tree-fix abnf::cst)) (cst-constraint-conc? abnf::cst)))
Theorem:
(defthm cst-constraint-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-constraint-conc? abnf::cst) (cst-constraint-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-constraint-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "constraint") (iff (equal (cst-constraint-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "equality-constraint"))))
Theorem:
(defthm cst-constraint-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "constraint") (iff (equal (cst-constraint-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "relation-constraint"))))
Function:
(defun cst-line-feed-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "line-feed"))) (let ((__function__ 'cst-line-feed-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-line-feed-conc (b* ((abnf::cstss (cst-line-feed-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-line-feed-conc-match (implies (cst-matchp abnf::cst "line-feed") (b* ((abnf::cstss (cst-line-feed-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%xA"))) :rule-classes :rewrite)
Theorem:
(defthm cst-line-feed-conc-of-tree-fix-cst (equal (cst-line-feed-conc (abnf::tree-fix abnf::cst)) (cst-line-feed-conc abnf::cst)))
Theorem:
(defthm cst-line-feed-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-line-feed-conc abnf::cst) (cst-line-feed-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-carriage-return-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "carriage-return"))) (let ((__function__ 'cst-carriage-return-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-carriage-return-conc (b* ((abnf::cstss (cst-carriage-return-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-carriage-return-conc-match (implies (cst-matchp abnf::cst "carriage-return") (b* ((abnf::cstss (cst-carriage-return-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%xD"))) :rule-classes :rewrite)
Theorem:
(defthm cst-carriage-return-conc-of-tree-fix-cst (equal (cst-carriage-return-conc (abnf::tree-fix abnf::cst)) (cst-carriage-return-conc abnf::cst)))
Theorem:
(defthm cst-carriage-return-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-carriage-return-conc abnf::cst) (cst-carriage-return-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-space-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "space"))) (let ((__function__ 'cst-space-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-space-conc (b* ((abnf::cstss (cst-space-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-space-conc-match (implies (cst-matchp abnf::cst "space") (b* ((abnf::cstss (cst-space-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x20"))) :rule-classes :rewrite)
Theorem:
(defthm cst-space-conc-of-tree-fix-cst (equal (cst-space-conc (abnf::tree-fix abnf::cst)) (cst-space-conc abnf::cst)))
Theorem:
(defthm cst-space-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-space-conc abnf::cst) (cst-space-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-line-terminator-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "line-terminator"))) (let ((__function__ 'cst-line-terminator-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-line-terminator-conc (b* ((abnf::cstss (cst-line-terminator-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-line-terminator-conc-match (implies (cst-matchp abnf::cst "line-terminator") (b* ((abnf::cstss (cst-line-terminator-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "[ carriage-return ] line-feed"))) :rule-classes :rewrite)
Theorem:
(defthm cst-line-terminator-conc-of-tree-fix-cst (equal (cst-line-terminator-conc (abnf::tree-fix abnf::cst)) (cst-line-terminator-conc abnf::cst)))
Theorem:
(defthm cst-line-terminator-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-line-terminator-conc abnf::cst) (cst-line-terminator-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-whitespace-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 1)))) (let ((__function__ 'cst-whitespace-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-whitespace-conc1 (b* ((abnf::cstss (cst-whitespace-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc1-match (implies (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-whitespace-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "space"))) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc1-of-tree-fix-cst (equal (cst-whitespace-conc1 (abnf::tree-fix abnf::cst)) (cst-whitespace-conc1 abnf::cst)))
Theorem:
(defthm cst-whitespace-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-whitespace-conc1 abnf::cst) (cst-whitespace-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-whitespace-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 2)))) (let ((__function__ 'cst-whitespace-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-whitespace-conc2 (b* ((abnf::cstss (cst-whitespace-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc2-match (implies (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-whitespace-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "line-terminator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc2-of-tree-fix-cst (equal (cst-whitespace-conc2 (abnf::tree-fix abnf::cst)) (cst-whitespace-conc2 abnf::cst)))
Theorem:
(defthm cst-whitespace-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-whitespace-conc2 abnf::cst) (cst-whitespace-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-uppercase-letter-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "uppercase-letter"))) (let ((__function__ 'cst-uppercase-letter-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-uppercase-letter-conc (b* ((abnf::cstss (cst-uppercase-letter-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-match (implies (cst-matchp abnf::cst "uppercase-letter") (b* ((abnf::cstss (cst-uppercase-letter-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x41-5A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-of-tree-fix-cst (equal (cst-uppercase-letter-conc (abnf::tree-fix abnf::cst)) (cst-uppercase-letter-conc abnf::cst)))
Theorem:
(defthm cst-uppercase-letter-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-uppercase-letter-conc abnf::cst) (cst-uppercase-letter-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lowercase-letter-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lowercase-letter"))) (let ((__function__ 'cst-lowercase-letter-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-lowercase-letter-conc (b* ((abnf::cstss (cst-lowercase-letter-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-match (implies (cst-matchp abnf::cst "lowercase-letter") (b* ((abnf::cstss (cst-lowercase-letter-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x61-7A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-of-tree-fix-cst (equal (cst-lowercase-letter-conc (abnf::tree-fix abnf::cst)) (cst-lowercase-letter-conc abnf::cst)))
Theorem:
(defthm cst-lowercase-letter-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lowercase-letter-conc abnf::cst) (cst-lowercase-letter-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-letter-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 1)))) (let ((__function__ 'cst-letter-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-letter-conc1 (b* ((abnf::cstss (cst-letter-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc1-match (implies (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-letter-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "uppercase-letter"))) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc1-of-tree-fix-cst (equal (cst-letter-conc1 (abnf::tree-fix abnf::cst)) (cst-letter-conc1 abnf::cst)))
Theorem:
(defthm cst-letter-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-letter-conc1 abnf::cst) (cst-letter-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-letter-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 2)))) (let ((__function__ 'cst-letter-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-letter-conc2 (b* ((abnf::cstss (cst-letter-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc2-match (implies (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-letter-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "lowercase-letter"))) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc2-of-tree-fix-cst (equal (cst-letter-conc2 (abnf::tree-fix abnf::cst)) (cst-letter-conc2 abnf::cst)))
Theorem:
(defthm cst-letter-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-letter-conc2 abnf::cst) (cst-letter-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-digit-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "digit"))) (let ((__function__ 'cst-digit-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-digit-conc (b* ((abnf::cstss (cst-digit-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-digit-conc-match (implies (cst-matchp abnf::cst "digit") (b* ((abnf::cstss (cst-digit-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-digit-conc-of-tree-fix-cst (equal (cst-digit-conc (abnf::tree-fix abnf::cst)) (cst-digit-conc abnf::cst)))
Theorem:
(defthm cst-digit-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-digit-conc abnf::cst) (cst-digit-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-numeral-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "numeral"))) (let ((__function__ 'cst-numeral-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-numeral-conc (b* ((abnf::cstss (cst-numeral-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-numeral-conc-match (implies (cst-matchp abnf::cst "numeral") (b* ((abnf::cstss (cst-numeral-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "1*digit"))) :rule-classes :rewrite)
Theorem:
(defthm cst-numeral-conc-of-tree-fix-cst (equal (cst-numeral-conc (abnf::tree-fix abnf::cst)) (cst-numeral-conc abnf::cst)))
Theorem:
(defthm cst-numeral-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-numeral-conc abnf::cst) (cst-numeral-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-identifier-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "identifier"))) (let ((__function__ 'cst-identifier-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-identifier-conc (b* ((abnf::cstss (cst-identifier-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-conc-match (implies (cst-matchp abnf::cst "identifier") (b* ((abnf::cstss (cst-identifier-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "letter *( letter / digit / \"_\" )"))) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-conc-of-tree-fix-cst (equal (cst-identifier-conc (abnf::tree-fix abnf::cst)) (cst-identifier-conc abnf::cst)))
Theorem:
(defthm cst-identifier-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-conc abnf::cst) (cst-identifier-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)))) (let ((__function__ 'cst-token-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-token-conc1 (b* ((abnf::cstss (cst-token-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-token-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "identifier"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-of-tree-fix-cst (equal (cst-token-conc1 (abnf::tree-fix abnf::cst)) (cst-token-conc1 abnf::cst)))
Theorem:
(defthm cst-token-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc1 abnf::cst) (cst-token-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)))) (let ((__function__ 'cst-token-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-token-conc2 (b* ((abnf::cstss (cst-token-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-token-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "numeral"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-of-tree-fix-cst (equal (cst-token-conc2 (abnf::tree-fix abnf::cst)) (cst-token-conc2 abnf::cst)))
Theorem:
(defthm cst-token-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc2 abnf::cst) (cst-token-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc3 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)))) (let ((__function__ 'cst-token-conc3)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-token-conc3 (b* ((abnf::cstss (cst-token-conc3 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)) (b* ((abnf::cstss (cst-token-conc3 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "operator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-of-tree-fix-cst (equal (cst-token-conc3 (abnf::tree-fix abnf::cst)) (cst-token-conc3 abnf::cst)))
Theorem:
(defthm cst-token-conc3-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc3 abnf::cst) (cst-token-conc3 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc4 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)))) (let ((__function__ 'cst-token-conc4)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-token-conc4 (b* ((abnf::cstss (cst-token-conc4 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)) (b* ((abnf::cstss (cst-token-conc4 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "separator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-of-tree-fix-cst (equal (cst-token-conc4 (abnf::tree-fix abnf::cst)) (cst-token-conc4 abnf::cst)))
Theorem:
(defthm cst-token-conc4-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc4 abnf::cst) (cst-token-conc4 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)))) (let ((__function__ 'cst-lexeme-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-lexeme-conc1 (b* ((abnf::cstss (cst-lexeme-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-lexeme-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "token"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-of-tree-fix-cst (equal (cst-lexeme-conc1 (abnf::tree-fix abnf::cst)) (cst-lexeme-conc1 abnf::cst)))
Theorem:
(defthm cst-lexeme-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc1 abnf::cst) (cst-lexeme-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)))) (let ((__function__ 'cst-lexeme-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-lexeme-conc2 (b* ((abnf::cstss (cst-lexeme-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-lexeme-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "whitespace"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-of-tree-fix-cst (equal (cst-lexeme-conc2 (abnf::tree-fix abnf::cst)) (cst-lexeme-conc2 abnf::cst)))
Theorem:
(defthm cst-lexeme-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc2 abnf::cst) (cst-lexeme-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-unary-minus-expression-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "unary-minus-expression"))) (let ((__function__ 'cst-unary-minus-expression-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-unary-minus-expression-conc (b* ((abnf::cstss (cst-unary-minus-expression-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-unary-minus-expression-conc-match (implies (cst-matchp abnf::cst "unary-minus-expression") (b* ((abnf::cstss (cst-unary-minus-expression-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "[ \"-\" ] primary-expression"))) :rule-classes :rewrite)
Theorem:
(defthm cst-unary-minus-expression-conc-of-tree-fix-cst (equal (cst-unary-minus-expression-conc (abnf::tree-fix abnf::cst)) (cst-unary-minus-expression-conc abnf::cst)))
Theorem:
(defthm cst-unary-minus-expression-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-unary-minus-expression-conc abnf::cst) (cst-unary-minus-expression-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "expression"))) (let ((__function__ 'cst-expression-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-expression-conc (b* ((abnf::cstss (cst-expression-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc-match (implies (cst-matchp abnf::cst "expression") (b* ((abnf::cstss (cst-expression-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "additive-expression"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc-of-tree-fix-cst (equal (cst-expression-conc (abnf::tree-fix abnf::cst)) (cst-expression-conc abnf::cst)))
Theorem:
(defthm cst-expression-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc abnf::cst) (cst-expression-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-equality-constraint-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "equality-constraint"))) (let ((__function__ 'cst-equality-constraint-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-equality-constraint-conc (b* ((abnf::cstss (cst-equality-constraint-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-equality-constraint-conc-match (implies (cst-matchp abnf::cst "equality-constraint") (b* ((abnf::cstss (cst-equality-constraint-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "expression \"==\" expression"))) :rule-classes :rewrite)
Theorem:
(defthm cst-equality-constraint-conc-of-tree-fix-cst (equal (cst-equality-constraint-conc (abnf::tree-fix abnf::cst)) (cst-equality-constraint-conc abnf::cst)))
Theorem:
(defthm cst-equality-constraint-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-equality-constraint-conc abnf::cst) (cst-equality-constraint-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-relation-constraint-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "relation-constraint"))) (let ((__function__ 'cst-relation-constraint-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-relation-constraint-conc (b* ((abnf::cstss (cst-relation-constraint-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-relation-constraint-conc-match (implies (cst-matchp abnf::cst "relation-constraint") (b* ((abnf::cstss (cst-relation-constraint-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "identifier \"(\" [ expression *( \",\" expression ) ] \")\""))) :rule-classes :rewrite)
Theorem:
(defthm cst-relation-constraint-conc-of-tree-fix-cst (equal (cst-relation-constraint-conc (abnf::tree-fix abnf::cst)) (cst-relation-constraint-conc abnf::cst)))
Theorem:
(defthm cst-relation-constraint-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-relation-constraint-conc abnf::cst) (cst-relation-constraint-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-constraint-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 1)))) (let ((__function__ 'cst-constraint-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-constraint-conc1 (b* ((abnf::cstss (cst-constraint-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc1-match (implies (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-constraint-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "equality-constraint"))) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc1-of-tree-fix-cst (equal (cst-constraint-conc1 (abnf::tree-fix abnf::cst)) (cst-constraint-conc1 abnf::cst)))
Theorem:
(defthm cst-constraint-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-constraint-conc1 abnf::cst) (cst-constraint-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-constraint-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 2)))) (let ((__function__ 'cst-constraint-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-constraint-conc2 (b* ((abnf::cstss (cst-constraint-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc2-match (implies (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-constraint-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "relation-constraint"))) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc2-of-tree-fix-cst (equal (cst-constraint-conc2 (abnf::tree-fix abnf::cst)) (cst-constraint-conc2 abnf::cst)))
Theorem:
(defthm cst-constraint-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-constraint-conc2 abnf::cst) (cst-constraint-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-definition-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "definition"))) (let ((__function__ 'cst-definition-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-definition-conc (b* ((abnf::cstss (cst-definition-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-definition-conc-match (implies (cst-matchp abnf::cst "definition") (b* ((abnf::cstss (cst-definition-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "identifier \"(\" [ identifier *( \",\" identifier ) ] \")\" \":=\" \"{\" [ constraint *( \",\" constraint ) ] \"}\""))) :rule-classes :rewrite)
Theorem:
(defthm cst-definition-conc-of-tree-fix-cst (equal (cst-definition-conc (abnf::tree-fix abnf::cst)) (cst-definition-conc abnf::cst)))
Theorem:
(defthm cst-definition-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-definition-conc abnf::cst) (cst-definition-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-system-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "system"))) (let ((__function__ 'cst-system-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-system-conc (b* ((abnf::cstss (cst-system-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-system-conc-match (implies (cst-matchp abnf::cst "system") (b* ((abnf::cstss (cst-system-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "*definition *constraint"))) :rule-classes :rewrite)
Theorem:
(defthm cst-system-conc-of-tree-fix-cst (equal (cst-system-conc (abnf::tree-fix abnf::cst)) (cst-system-conc abnf::cst)))
Theorem:
(defthm cst-system-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-system-conc abnf::cst) (cst-system-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-line-feed-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "line-feed"))) (let ((__function__ 'cst-line-feed-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-line-feed-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-line-feed-conc-rep (b* ((abnf::csts (cst-line-feed-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-line-feed-conc-rep-match (implies (cst-matchp abnf::cst "line-feed") (b* ((abnf::csts (cst-line-feed-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%xA"))) :rule-classes :rewrite)
Theorem:
(defthm cst-line-feed-conc-rep-of-tree-fix-cst (equal (cst-line-feed-conc-rep (abnf::tree-fix abnf::cst)) (cst-line-feed-conc-rep abnf::cst)))
Theorem:
(defthm cst-line-feed-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-line-feed-conc-rep abnf::cst) (cst-line-feed-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-carriage-return-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "carriage-return"))) (let ((__function__ 'cst-carriage-return-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-carriage-return-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-carriage-return-conc-rep (b* ((abnf::csts (cst-carriage-return-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-carriage-return-conc-rep-match (implies (cst-matchp abnf::cst "carriage-return") (b* ((abnf::csts (cst-carriage-return-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%xD"))) :rule-classes :rewrite)
Theorem:
(defthm cst-carriage-return-conc-rep-of-tree-fix-cst (equal (cst-carriage-return-conc-rep (abnf::tree-fix abnf::cst)) (cst-carriage-return-conc-rep abnf::cst)))
Theorem:
(defthm cst-carriage-return-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-carriage-return-conc-rep abnf::cst) (cst-carriage-return-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-space-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "space"))) (let ((__function__ 'cst-space-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-space-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-space-conc-rep (b* ((abnf::csts (cst-space-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-space-conc-rep-match (implies (cst-matchp abnf::cst "space") (b* ((abnf::csts (cst-space-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x20"))) :rule-classes :rewrite)
Theorem:
(defthm cst-space-conc-rep-of-tree-fix-cst (equal (cst-space-conc-rep (abnf::tree-fix abnf::cst)) (cst-space-conc-rep abnf::cst)))
Theorem:
(defthm cst-space-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-space-conc-rep abnf::cst) (cst-space-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-whitespace-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 1)))) (let ((__function__ 'cst-whitespace-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-whitespace-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-whitespace-conc1-rep (b* ((abnf::csts (cst-whitespace-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc1-rep-match (implies (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-whitespace-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "space"))) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc1-rep-of-tree-fix-cst (equal (cst-whitespace-conc1-rep (abnf::tree-fix abnf::cst)) (cst-whitespace-conc1-rep abnf::cst)))
Theorem:
(defthm cst-whitespace-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-whitespace-conc1-rep abnf::cst) (cst-whitespace-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-whitespace-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 2)))) (let ((__function__ 'cst-whitespace-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-whitespace-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-whitespace-conc2-rep (b* ((abnf::csts (cst-whitespace-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc2-rep-match (implies (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-whitespace-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "line-terminator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc2-rep-of-tree-fix-cst (equal (cst-whitespace-conc2-rep (abnf::tree-fix abnf::cst)) (cst-whitespace-conc2-rep abnf::cst)))
Theorem:
(defthm cst-whitespace-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-whitespace-conc2-rep abnf::cst) (cst-whitespace-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-uppercase-letter-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "uppercase-letter"))) (let ((__function__ 'cst-uppercase-letter-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-uppercase-letter-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-uppercase-letter-conc-rep (b* ((abnf::csts (cst-uppercase-letter-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-rep-match (implies (cst-matchp abnf::cst "uppercase-letter") (b* ((abnf::csts (cst-uppercase-letter-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x41-5A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-rep-of-tree-fix-cst (equal (cst-uppercase-letter-conc-rep (abnf::tree-fix abnf::cst)) (cst-uppercase-letter-conc-rep abnf::cst)))
Theorem:
(defthm cst-uppercase-letter-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-uppercase-letter-conc-rep abnf::cst) (cst-uppercase-letter-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lowercase-letter-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lowercase-letter"))) (let ((__function__ 'cst-lowercase-letter-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-lowercase-letter-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-lowercase-letter-conc-rep (b* ((abnf::csts (cst-lowercase-letter-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-rep-match (implies (cst-matchp abnf::cst "lowercase-letter") (b* ((abnf::csts (cst-lowercase-letter-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x61-7A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-rep-of-tree-fix-cst (equal (cst-lowercase-letter-conc-rep (abnf::tree-fix abnf::cst)) (cst-lowercase-letter-conc-rep abnf::cst)))
Theorem:
(defthm cst-lowercase-letter-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lowercase-letter-conc-rep abnf::cst) (cst-lowercase-letter-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-letter-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 1)))) (let ((__function__ 'cst-letter-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-letter-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-letter-conc1-rep (b* ((abnf::csts (cst-letter-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc1-rep-match (implies (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-letter-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "uppercase-letter"))) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc1-rep-of-tree-fix-cst (equal (cst-letter-conc1-rep (abnf::tree-fix abnf::cst)) (cst-letter-conc1-rep abnf::cst)))
Theorem:
(defthm cst-letter-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-letter-conc1-rep abnf::cst) (cst-letter-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-letter-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 2)))) (let ((__function__ 'cst-letter-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-letter-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-letter-conc2-rep (b* ((abnf::csts (cst-letter-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc2-rep-match (implies (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-letter-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "lowercase-letter"))) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc2-rep-of-tree-fix-cst (equal (cst-letter-conc2-rep (abnf::tree-fix abnf::cst)) (cst-letter-conc2-rep abnf::cst)))
Theorem:
(defthm cst-letter-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-letter-conc2-rep abnf::cst) (cst-letter-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-digit-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "digit"))) (let ((__function__ 'cst-digit-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-digit-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-digit-conc-rep (b* ((abnf::csts (cst-digit-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-digit-conc-rep-match (implies (cst-matchp abnf::cst "digit") (b* ((abnf::csts (cst-digit-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-digit-conc-rep-of-tree-fix-cst (equal (cst-digit-conc-rep (abnf::tree-fix abnf::cst)) (cst-digit-conc-rep abnf::cst)))
Theorem:
(defthm cst-digit-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-digit-conc-rep abnf::cst) (cst-digit-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)))) (let ((__function__ 'cst-token-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-token-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-token-conc1-rep (b* ((abnf::csts (cst-token-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-rep-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-token-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "identifier"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-rep-of-tree-fix-cst (equal (cst-token-conc1-rep (abnf::tree-fix abnf::cst)) (cst-token-conc1-rep abnf::cst)))
Theorem:
(defthm cst-token-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc1-rep abnf::cst) (cst-token-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)))) (let ((__function__ 'cst-token-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-token-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-token-conc2-rep (b* ((abnf::csts (cst-token-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-rep-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-token-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "numeral"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-rep-of-tree-fix-cst (equal (cst-token-conc2-rep (abnf::tree-fix abnf::cst)) (cst-token-conc2-rep abnf::cst)))
Theorem:
(defthm cst-token-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc2-rep abnf::cst) (cst-token-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc3-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)))) (let ((__function__ 'cst-token-conc3-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-token-conc3 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-token-conc3-rep (b* ((abnf::csts (cst-token-conc3-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-rep-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)) (b* ((abnf::csts (cst-token-conc3-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "operator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-rep-of-tree-fix-cst (equal (cst-token-conc3-rep (abnf::tree-fix abnf::cst)) (cst-token-conc3-rep abnf::cst)))
Theorem:
(defthm cst-token-conc3-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc3-rep abnf::cst) (cst-token-conc3-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc4-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)))) (let ((__function__ 'cst-token-conc4-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-token-conc4 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-token-conc4-rep (b* ((abnf::csts (cst-token-conc4-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-rep-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)) (b* ((abnf::csts (cst-token-conc4-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "separator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-rep-of-tree-fix-cst (equal (cst-token-conc4-rep (abnf::tree-fix abnf::cst)) (cst-token-conc4-rep abnf::cst)))
Theorem:
(defthm cst-token-conc4-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc4-rep abnf::cst) (cst-token-conc4-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)))) (let ((__function__ 'cst-lexeme-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-lexeme-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-lexeme-conc1-rep (b* ((abnf::csts (cst-lexeme-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-rep-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-lexeme-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "token"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-rep-of-tree-fix-cst (equal (cst-lexeme-conc1-rep (abnf::tree-fix abnf::cst)) (cst-lexeme-conc1-rep abnf::cst)))
Theorem:
(defthm cst-lexeme-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc1-rep abnf::cst) (cst-lexeme-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)))) (let ((__function__ 'cst-lexeme-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-lexeme-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-lexeme-conc2-rep (b* ((abnf::csts (cst-lexeme-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-rep-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-lexeme-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "whitespace"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-rep-of-tree-fix-cst (equal (cst-lexeme-conc2-rep (abnf::tree-fix abnf::cst)) (cst-lexeme-conc2-rep abnf::cst)))
Theorem:
(defthm cst-lexeme-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc2-rep abnf::cst) (cst-lexeme-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "expression"))) (let ((__function__ 'cst-expression-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-expression-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-expression-conc-rep (b* ((abnf::csts (cst-expression-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc-rep-match (implies (cst-matchp abnf::cst "expression") (b* ((abnf::csts (cst-expression-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "additive-expression"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc-rep-of-tree-fix-cst (equal (cst-expression-conc-rep (abnf::tree-fix abnf::cst)) (cst-expression-conc-rep abnf::cst)))
Theorem:
(defthm cst-expression-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc-rep abnf::cst) (cst-expression-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-constraint-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 1)))) (let ((__function__ 'cst-constraint-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-constraint-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-constraint-conc1-rep (b* ((abnf::csts (cst-constraint-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc1-rep-match (implies (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-constraint-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "equality-constraint"))) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc1-rep-of-tree-fix-cst (equal (cst-constraint-conc1-rep (abnf::tree-fix abnf::cst)) (cst-constraint-conc1-rep abnf::cst)))
Theorem:
(defthm cst-constraint-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-constraint-conc1-rep abnf::cst) (cst-constraint-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-constraint-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 2)))) (let ((__function__ 'cst-constraint-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-constraint-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-constraint-conc2-rep (b* ((abnf::csts (cst-constraint-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc2-rep-match (implies (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-constraint-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "relation-constraint"))) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc2-rep-of-tree-fix-cst (equal (cst-constraint-conc2-rep (abnf::tree-fix abnf::cst)) (cst-constraint-conc2-rep abnf::cst)))
Theorem:
(defthm cst-constraint-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-constraint-conc2-rep abnf::cst) (cst-constraint-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-line-feed-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "line-feed"))) (let ((__function__ 'cst-line-feed-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-line-feed-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-line-feed-conc-rep-elem (b* ((abnf::cst1 (cst-line-feed-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-line-feed-conc-rep-elem-match (implies (cst-matchp abnf::cst "line-feed") (b* ((abnf::cst1 (cst-line-feed-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%xA"))) :rule-classes :rewrite)
Theorem:
(defthm cst-line-feed-conc-rep-elem-of-tree-fix-cst (equal (cst-line-feed-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-line-feed-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-line-feed-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-line-feed-conc-rep-elem abnf::cst) (cst-line-feed-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-carriage-return-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "carriage-return"))) (let ((__function__ 'cst-carriage-return-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-carriage-return-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-carriage-return-conc-rep-elem (b* ((abnf::cst1 (cst-carriage-return-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-carriage-return-conc-rep-elem-match (implies (cst-matchp abnf::cst "carriage-return") (b* ((abnf::cst1 (cst-carriage-return-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%xD"))) :rule-classes :rewrite)
Theorem:
(defthm cst-carriage-return-conc-rep-elem-of-tree-fix-cst (equal (cst-carriage-return-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-carriage-return-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-carriage-return-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-carriage-return-conc-rep-elem abnf::cst) (cst-carriage-return-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-space-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "space"))) (let ((__function__ 'cst-space-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-space-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-space-conc-rep-elem (b* ((abnf::cst1 (cst-space-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-space-conc-rep-elem-match (implies (cst-matchp abnf::cst "space") (b* ((abnf::cst1 (cst-space-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x20"))) :rule-classes :rewrite)
Theorem:
(defthm cst-space-conc-rep-elem-of-tree-fix-cst (equal (cst-space-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-space-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-space-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-space-conc-rep-elem abnf::cst) (cst-space-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-whitespace-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 1)))) (let ((__function__ 'cst-whitespace-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-whitespace-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-whitespace-conc1-rep-elem (b* ((abnf::cst1 (cst-whitespace-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-whitespace-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "space"))) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc1-rep-elem-of-tree-fix-cst (equal (cst-whitespace-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-whitespace-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-whitespace-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-whitespace-conc1-rep-elem abnf::cst) (cst-whitespace-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-whitespace-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 2)))) (let ((__function__ 'cst-whitespace-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-whitespace-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-whitespace-conc2-rep-elem (b* ((abnf::cst1 (cst-whitespace-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "whitespace") (equal (cst-whitespace-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-whitespace-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "line-terminator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc2-rep-elem-of-tree-fix-cst (equal (cst-whitespace-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-whitespace-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-whitespace-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-whitespace-conc2-rep-elem abnf::cst) (cst-whitespace-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-uppercase-letter-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "uppercase-letter"))) (let ((__function__ 'cst-uppercase-letter-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-uppercase-letter-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-uppercase-letter-conc-rep-elem (b* ((abnf::cst1 (cst-uppercase-letter-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-rep-elem-match (implies (cst-matchp abnf::cst "uppercase-letter") (b* ((abnf::cst1 (cst-uppercase-letter-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x41-5A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-rep-elem-of-tree-fix-cst (equal (cst-uppercase-letter-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-uppercase-letter-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-uppercase-letter-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-uppercase-letter-conc-rep-elem abnf::cst) (cst-uppercase-letter-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lowercase-letter-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lowercase-letter"))) (let ((__function__ 'cst-lowercase-letter-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-lowercase-letter-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-lowercase-letter-conc-rep-elem (b* ((abnf::cst1 (cst-lowercase-letter-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-rep-elem-match (implies (cst-matchp abnf::cst "lowercase-letter") (b* ((abnf::cst1 (cst-lowercase-letter-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x61-7A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-rep-elem-of-tree-fix-cst (equal (cst-lowercase-letter-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-lowercase-letter-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-lowercase-letter-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lowercase-letter-conc-rep-elem abnf::cst) (cst-lowercase-letter-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-letter-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 1)))) (let ((__function__ 'cst-letter-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-letter-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-letter-conc1-rep-elem (b* ((abnf::cst1 (cst-letter-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-letter-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "uppercase-letter"))) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc1-rep-elem-of-tree-fix-cst (equal (cst-letter-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-letter-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-letter-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-letter-conc1-rep-elem abnf::cst) (cst-letter-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-letter-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 2)))) (let ((__function__ 'cst-letter-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-letter-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-letter-conc2-rep-elem (b* ((abnf::cst1 (cst-letter-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "letter") (equal (cst-letter-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-letter-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "lowercase-letter"))) :rule-classes :rewrite)
Theorem:
(defthm cst-letter-conc2-rep-elem-of-tree-fix-cst (equal (cst-letter-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-letter-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-letter-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-letter-conc2-rep-elem abnf::cst) (cst-letter-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-digit-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "digit"))) (let ((__function__ 'cst-digit-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-digit-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-digit-conc-rep-elem (b* ((abnf::cst1 (cst-digit-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-digit-conc-rep-elem-match (implies (cst-matchp abnf::cst "digit") (b* ((abnf::cst1 (cst-digit-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-digit-conc-rep-elem-of-tree-fix-cst (equal (cst-digit-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-digit-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-digit-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-digit-conc-rep-elem abnf::cst) (cst-digit-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)))) (let ((__function__ 'cst-token-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-token-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-token-conc1-rep-elem (b* ((abnf::cst1 (cst-token-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-token-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "identifier"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-rep-elem-of-tree-fix-cst (equal (cst-token-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-token-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-token-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc1-rep-elem abnf::cst) (cst-token-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)))) (let ((__function__ 'cst-token-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-token-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-token-conc2-rep-elem (b* ((abnf::cst1 (cst-token-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-token-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "numeral"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-rep-elem-of-tree-fix-cst (equal (cst-token-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-token-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-token-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc2-rep-elem abnf::cst) (cst-token-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc3-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)))) (let ((__function__ 'cst-token-conc3-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-token-conc3-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-token-conc3-rep-elem (b* ((abnf::cst1 (cst-token-conc3-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-rep-elem-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)) (b* ((abnf::cst1 (cst-token-conc3-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "operator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-rep-elem-of-tree-fix-cst (equal (cst-token-conc3-rep-elem (abnf::tree-fix abnf::cst)) (cst-token-conc3-rep-elem abnf::cst)))
Theorem:
(defthm cst-token-conc3-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc3-rep-elem abnf::cst) (cst-token-conc3-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc4-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)))) (let ((__function__ 'cst-token-conc4-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-token-conc4-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-token-conc4-rep-elem (b* ((abnf::cst1 (cst-token-conc4-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-rep-elem-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)) (b* ((abnf::cst1 (cst-token-conc4-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "separator"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-rep-elem-of-tree-fix-cst (equal (cst-token-conc4-rep-elem (abnf::tree-fix abnf::cst)) (cst-token-conc4-rep-elem abnf::cst)))
Theorem:
(defthm cst-token-conc4-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc4-rep-elem abnf::cst) (cst-token-conc4-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)))) (let ((__function__ 'cst-lexeme-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-lexeme-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-lexeme-conc1-rep-elem (b* ((abnf::cst1 (cst-lexeme-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-lexeme-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "token"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-rep-elem-of-tree-fix-cst (equal (cst-lexeme-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-lexeme-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-lexeme-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc1-rep-elem abnf::cst) (cst-lexeme-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)))) (let ((__function__ 'cst-lexeme-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-lexeme-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-lexeme-conc2-rep-elem (b* ((abnf::cst1 (cst-lexeme-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-lexeme-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "whitespace"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-rep-elem-of-tree-fix-cst (equal (cst-lexeme-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-lexeme-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-lexeme-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc2-rep-elem abnf::cst) (cst-lexeme-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "expression"))) (let ((__function__ 'cst-expression-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-expression-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-expression-conc-rep-elem (b* ((abnf::cst1 (cst-expression-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc-rep-elem-match (implies (cst-matchp abnf::cst "expression") (b* ((abnf::cst1 (cst-expression-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "additive-expression"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc-rep-elem-of-tree-fix-cst (equal (cst-expression-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-expression-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-expression-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc-rep-elem abnf::cst) (cst-expression-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-constraint-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 1)))) (let ((__function__ 'cst-constraint-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-constraint-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-constraint-conc1-rep-elem (b* ((abnf::cst1 (cst-constraint-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-constraint-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "equality-constraint"))) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc1-rep-elem-of-tree-fix-cst (equal (cst-constraint-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-constraint-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-constraint-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-constraint-conc1-rep-elem abnf::cst) (cst-constraint-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-constraint-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 2)))) (let ((__function__ 'cst-constraint-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-constraint-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-constraint-conc2-rep-elem (b* ((abnf::cst1 (cst-constraint-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "constraint") (equal (cst-constraint-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-constraint-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "relation-constraint"))) :rule-classes :rewrite)
Theorem:
(defthm cst-constraint-conc2-rep-elem-of-tree-fix-cst (equal (cst-constraint-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-constraint-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-constraint-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-constraint-conc2-rep-elem abnf::cst) (cst-constraint-conc2-rep-elem cst-equiv))) :rule-classes :congruence)