Tree operations specialized to *all-grammar-rules*.
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 *all-grammar-rules*))))
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 *all-grammar-rules*))))
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 *all-grammar-rules*))))
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 *all-grammar-rules*))))
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 *all-grammar-rules*))))
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)
Theorem:
(defthm cst-json-text-nonleaf (implies (cst-matchp abnf::cst "json-text") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-begin-array-nonleaf (implies (cst-matchp abnf::cst "begin-array") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-begin-object-nonleaf (implies (cst-matchp abnf::cst "begin-object") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-end-array-nonleaf (implies (cst-matchp abnf::cst "end-array") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-end-object-nonleaf (implies (cst-matchp abnf::cst "end-object") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-name-separator-nonleaf (implies (cst-matchp abnf::cst "name-separator") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-value-separator-nonleaf (implies (cst-matchp abnf::cst "value-separator") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-ws-nonleaf (implies (cst-matchp abnf::cst "ws") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-value-nonleaf (implies (cst-matchp abnf::cst "value") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-false-nonleaf (implies (cst-matchp abnf::cst "false") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-null-nonleaf (implies (cst-matchp abnf::cst "null") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-true-nonleaf (implies (cst-matchp abnf::cst "true") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-object-nonleaf (implies (cst-matchp abnf::cst "object") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-member-nonleaf (implies (cst-matchp abnf::cst "member") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-array-nonleaf (implies (cst-matchp abnf::cst "array") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-number-nonleaf (implies (cst-matchp abnf::cst "number") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-decimal-point-nonleaf (implies (cst-matchp abnf::cst "decimal-point") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-digit1-9-nonleaf (implies (cst-matchp abnf::cst "digit1-9") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-e-nonleaf (implies (cst-matchp abnf::cst "e") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-exp-nonleaf (implies (cst-matchp abnf::cst "exp") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-frac-nonleaf (implies (cst-matchp abnf::cst "frac") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-int-nonleaf (implies (cst-matchp abnf::cst "int") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-minus-nonleaf (implies (cst-matchp abnf::cst "minus") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-plus-nonleaf (implies (cst-matchp abnf::cst "plus") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-zero-nonleaf (implies (cst-matchp abnf::cst "zero") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-string-nonleaf (implies (cst-matchp abnf::cst "string") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-char-nonleaf (implies (cst-matchp abnf::cst "char") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-escape-nonleaf (implies (cst-matchp abnf::cst "escape") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-quotation-mark-nonleaf (implies (cst-matchp abnf::cst "quotation-mark") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-unescaped-nonleaf (implies (cst-matchp abnf::cst "unescaped") (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-hexdig-nonleaf (implies (cst-matchp abnf::cst "hexdig") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-json-text-rulename (implies (cst-matchp abnf::cst "json-text") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "json-text"))))
Theorem:
(defthm cst-begin-array-rulename (implies (cst-matchp abnf::cst "begin-array") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "begin-array"))))
Theorem:
(defthm cst-begin-object-rulename (implies (cst-matchp abnf::cst "begin-object") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "begin-object"))))
Theorem:
(defthm cst-end-array-rulename (implies (cst-matchp abnf::cst "end-array") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "end-array"))))
Theorem:
(defthm cst-end-object-rulename (implies (cst-matchp abnf::cst "end-object") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "end-object"))))
Theorem:
(defthm cst-name-separator-rulename (implies (cst-matchp abnf::cst "name-separator") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "name-separator"))))
Theorem:
(defthm cst-value-separator-rulename (implies (cst-matchp abnf::cst "value-separator") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "value-separator"))))
Theorem:
(defthm cst-ws-rulename (implies (cst-matchp abnf::cst "ws") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "ws"))))
Theorem:
(defthm cst-value-rulename (implies (cst-matchp abnf::cst "value") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "value"))))
Theorem:
(defthm cst-false-rulename (implies (cst-matchp abnf::cst "false") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "false"))))
Theorem:
(defthm cst-null-rulename (implies (cst-matchp abnf::cst "null") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "null"))))
Theorem:
(defthm cst-true-rulename (implies (cst-matchp abnf::cst "true") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "true"))))
Theorem:
(defthm cst-object-rulename (implies (cst-matchp abnf::cst "object") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "object"))))
Theorem:
(defthm cst-member-rulename (implies (cst-matchp abnf::cst "member") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "member"))))
Theorem:
(defthm cst-array-rulename (implies (cst-matchp abnf::cst "array") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "array"))))
Theorem:
(defthm cst-number-rulename (implies (cst-matchp abnf::cst "number") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "number"))))
Theorem:
(defthm cst-decimal-point-rulename (implies (cst-matchp abnf::cst "decimal-point") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "decimal-point"))))
Theorem:
(defthm cst-digit1-9-rulename (implies (cst-matchp abnf::cst "digit1-9") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "digit1-9"))))
Theorem:
(defthm cst-e-rulename (implies (cst-matchp abnf::cst "e") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "e"))))
Theorem:
(defthm cst-exp-rulename (implies (cst-matchp abnf::cst "exp") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "exp"))))
Theorem:
(defthm cst-frac-rulename (implies (cst-matchp abnf::cst "frac") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "frac"))))
Theorem:
(defthm cst-int-rulename (implies (cst-matchp abnf::cst "int") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "int"))))
Theorem:
(defthm cst-minus-rulename (implies (cst-matchp abnf::cst "minus") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "minus"))))
Theorem:
(defthm cst-plus-rulename (implies (cst-matchp abnf::cst "plus") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "plus"))))
Theorem:
(defthm cst-zero-rulename (implies (cst-matchp abnf::cst "zero") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "zero"))))
Theorem:
(defthm cst-string-rulename (implies (cst-matchp abnf::cst "string") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "string"))))
Theorem:
(defthm cst-char-rulename (implies (cst-matchp abnf::cst "char") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "char"))))
Theorem:
(defthm cst-escape-rulename (implies (cst-matchp abnf::cst "escape") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "escape"))))
Theorem:
(defthm cst-quotation-mark-rulename (implies (cst-matchp abnf::cst "quotation-mark") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "quotation-mark"))))
Theorem:
(defthm cst-unescaped-rulename (implies (cst-matchp abnf::cst "unescaped") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "unescaped"))))
Theorem:
(defthm cst-digit-rulename (implies (cst-matchp abnf::cst "digit") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "digit"))))
Theorem:
(defthm cst-hexdig-rulename (implies (cst-matchp abnf::cst "hexdig") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "hexdig"))))
Theorem:
(defthm cst-json-text-branches-match-alt (implies (cst-matchp abnf::cst "json-text") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "ws value ws")))
Theorem:
(defthm cst-begin-array-branches-match-alt (implies (cst-matchp abnf::cst "begin-array") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "ws %x5B ws")))
Theorem:
(defthm cst-begin-object-branches-match-alt (implies (cst-matchp abnf::cst "begin-object") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "ws %x7B ws")))
Theorem:
(defthm cst-end-array-branches-match-alt (implies (cst-matchp abnf::cst "end-array") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "ws %x5D ws")))
Theorem:
(defthm cst-end-object-branches-match-alt (implies (cst-matchp abnf::cst "end-object") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "ws %x7D ws")))
Theorem:
(defthm cst-name-separator-branches-match-alt (implies (cst-matchp abnf::cst "name-separator") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "ws %x3A ws")))
Theorem:
(defthm cst-value-separator-branches-match-alt (implies (cst-matchp abnf::cst "value-separator") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "ws %x2C ws")))
Theorem:
(defthm cst-ws-branches-match-alt (implies (cst-matchp abnf::cst "ws") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "*( %x20 / %x9 / %xA / %xD )")))
Theorem:
(defthm cst-value-branches-match-alt (implies (cst-matchp abnf::cst "value") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "false / null / true / object / array / number / string")))
Theorem:
(defthm cst-false-branches-match-alt (implies (cst-matchp abnf::cst "false") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x66.61.6C.73.65")))
Theorem:
(defthm cst-null-branches-match-alt (implies (cst-matchp abnf::cst "null") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x6E.75.6C.6C")))
Theorem:
(defthm cst-true-branches-match-alt (implies (cst-matchp abnf::cst "true") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x74.72.75.65")))
Theorem:
(defthm cst-object-branches-match-alt (implies (cst-matchp abnf::cst "object") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "begin-object [ member *( value-separator member ) ] end-object")))
Theorem:
(defthm cst-member-branches-match-alt (implies (cst-matchp abnf::cst "member") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "string name-separator value")))
Theorem:
(defthm cst-array-branches-match-alt (implies (cst-matchp abnf::cst "array") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "begin-array [ value *( value-separator value ) ] end-array")))
Theorem:
(defthm cst-number-branches-match-alt (implies (cst-matchp abnf::cst "number") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "[ minus ] int [ frac ] [ exp ]")))
Theorem:
(defthm cst-decimal-point-branches-match-alt (implies (cst-matchp abnf::cst "decimal-point") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x2E")))
Theorem:
(defthm cst-digit1-9-branches-match-alt (implies (cst-matchp abnf::cst "digit1-9") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x31-39")))
Theorem:
(defthm cst-e-branches-match-alt (implies (cst-matchp abnf::cst "e") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x65 / %x45")))
Theorem:
(defthm cst-exp-branches-match-alt (implies (cst-matchp abnf::cst "exp") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "e [ minus / plus ] 1*digit")))
Theorem:
(defthm cst-frac-branches-match-alt (implies (cst-matchp abnf::cst "frac") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "decimal-point 1*digit")))
Theorem:
(defthm cst-int-branches-match-alt (implies (cst-matchp abnf::cst "int") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "zero / ( digit1-9 *digit )")))
Theorem:
(defthm cst-minus-branches-match-alt (implies (cst-matchp abnf::cst "minus") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x2D")))
Theorem:
(defthm cst-plus-branches-match-alt (implies (cst-matchp abnf::cst "plus") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x2B")))
Theorem:
(defthm cst-zero-branches-match-alt (implies (cst-matchp abnf::cst "zero") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x30")))
Theorem:
(defthm cst-string-branches-match-alt (implies (cst-matchp abnf::cst "string") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "quotation-mark *char quotation-mark")))
Theorem:
(defthm cst-char-branches-match-alt (implies (cst-matchp abnf::cst "char") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "unescaped / escape ( %x22 / %x5C / %x2F / %x62 / %x66 / %x6E / %x72 / %x74 / %x75 4hexdig )")))
Theorem:
(defthm cst-escape-branches-match-alt (implies (cst-matchp abnf::cst "escape") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x5C")))
Theorem:
(defthm cst-quotation-mark-branches-match-alt (implies (cst-matchp abnf::cst "quotation-mark") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x22")))
Theorem:
(defthm cst-unescaped-branches-match-alt (implies (cst-matchp abnf::cst "unescaped") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x20-21 / %x23-5B / %x5D-10FFFF")))
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-hexdig-branches-match-alt (implies (cst-matchp abnf::cst "hexdig") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "digit / \"A\" / \"B\" / \"C\" / \"D\" / \"E\" / \"F\"")))
Theorem:
(defthm cst-json-text-concs (implies (cst-list-list-alt-matchp abnf::cstss "ws value ws") (or (cst-list-list-conc-matchp abnf::cstss "ws value ws"))))
Theorem:
(defthm cst-begin-array-concs (implies (cst-list-list-alt-matchp abnf::cstss "ws %x5B ws") (or (cst-list-list-conc-matchp abnf::cstss "ws %x5B ws"))))
Theorem:
(defthm cst-begin-object-concs (implies (cst-list-list-alt-matchp abnf::cstss "ws %x7B ws") (or (cst-list-list-conc-matchp abnf::cstss "ws %x7B ws"))))
Theorem:
(defthm cst-end-array-concs (implies (cst-list-list-alt-matchp abnf::cstss "ws %x5D ws") (or (cst-list-list-conc-matchp abnf::cstss "ws %x5D ws"))))
Theorem:
(defthm cst-end-object-concs (implies (cst-list-list-alt-matchp abnf::cstss "ws %x7D ws") (or (cst-list-list-conc-matchp abnf::cstss "ws %x7D ws"))))
Theorem:
(defthm cst-name-separator-concs (implies (cst-list-list-alt-matchp abnf::cstss "ws %x3A ws") (or (cst-list-list-conc-matchp abnf::cstss "ws %x3A ws"))))
Theorem:
(defthm cst-value-separator-concs (implies (cst-list-list-alt-matchp abnf::cstss "ws %x2C ws") (or (cst-list-list-conc-matchp abnf::cstss "ws %x2C ws"))))
Theorem:
(defthm cst-ws-concs (implies (cst-list-list-alt-matchp abnf::cstss "*( %x20 / %x9 / %xA / %xD )") (or (cst-list-list-conc-matchp abnf::cstss "*( %x20 / %x9 / %xA / %xD )"))))
Theorem:
(defthm cst-value-concs (implies (cst-list-list-alt-matchp abnf::cstss "false / null / true / object / array / number / string") (or (cst-list-list-conc-matchp abnf::cstss "false") (cst-list-list-conc-matchp abnf::cstss "null") (cst-list-list-conc-matchp abnf::cstss "true") (cst-list-list-conc-matchp abnf::cstss "object") (cst-list-list-conc-matchp abnf::cstss "array") (cst-list-list-conc-matchp abnf::cstss "number") (cst-list-list-conc-matchp abnf::cstss "string"))))
Theorem:
(defthm cst-false-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x66.61.6C.73.65") (or (cst-list-list-conc-matchp abnf::cstss "%x66.61.6C.73.65"))))
Theorem:
(defthm cst-null-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x6E.75.6C.6C") (or (cst-list-list-conc-matchp abnf::cstss "%x6E.75.6C.6C"))))
Theorem:
(defthm cst-true-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x74.72.75.65") (or (cst-list-list-conc-matchp abnf::cstss "%x74.72.75.65"))))
Theorem:
(defthm cst-object-concs (implies (cst-list-list-alt-matchp abnf::cstss "begin-object [ member *( value-separator member ) ] end-object") (or (cst-list-list-conc-matchp abnf::cstss "begin-object [ member *( value-separator member ) ] end-object"))))
Theorem:
(defthm cst-member-concs (implies (cst-list-list-alt-matchp abnf::cstss "string name-separator value") (or (cst-list-list-conc-matchp abnf::cstss "string name-separator value"))))
Theorem:
(defthm cst-array-concs (implies (cst-list-list-alt-matchp abnf::cstss "begin-array [ value *( value-separator value ) ] end-array") (or (cst-list-list-conc-matchp abnf::cstss "begin-array [ value *( value-separator value ) ] end-array"))))
Theorem:
(defthm cst-number-concs (implies (cst-list-list-alt-matchp abnf::cstss "[ minus ] int [ frac ] [ exp ]") (or (cst-list-list-conc-matchp abnf::cstss "[ minus ] int [ frac ] [ exp ]"))))
Theorem:
(defthm cst-decimal-point-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x2E") (or (cst-list-list-conc-matchp abnf::cstss "%x2E"))))
Theorem:
(defthm cst-digit1-9-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x31-39") (or (cst-list-list-conc-matchp abnf::cstss "%x31-39"))))
Theorem:
(defthm cst-e-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x65 / %x45") (or (cst-list-list-conc-matchp abnf::cstss "%x65") (cst-list-list-conc-matchp abnf::cstss "%x45"))))
Theorem:
(defthm cst-exp-concs (implies (cst-list-list-alt-matchp abnf::cstss "e [ minus / plus ] 1*digit") (or (cst-list-list-conc-matchp abnf::cstss "e [ minus / plus ] 1*digit"))))
Theorem:
(defthm cst-frac-concs (implies (cst-list-list-alt-matchp abnf::cstss "decimal-point 1*digit") (or (cst-list-list-conc-matchp abnf::cstss "decimal-point 1*digit"))))
Theorem:
(defthm cst-int-concs (implies (cst-list-list-alt-matchp abnf::cstss "zero / ( digit1-9 *digit )") (or (cst-list-list-conc-matchp abnf::cstss "zero") (cst-list-list-conc-matchp abnf::cstss "( digit1-9 *digit )"))))
Theorem:
(defthm cst-minus-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x2D") (or (cst-list-list-conc-matchp abnf::cstss "%x2D"))))
Theorem:
(defthm cst-plus-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x2B") (or (cst-list-list-conc-matchp abnf::cstss "%x2B"))))
Theorem:
(defthm cst-zero-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x30") (or (cst-list-list-conc-matchp abnf::cstss "%x30"))))
Theorem:
(defthm cst-string-concs (implies (cst-list-list-alt-matchp abnf::cstss "quotation-mark *char quotation-mark") (or (cst-list-list-conc-matchp abnf::cstss "quotation-mark *char quotation-mark"))))
Theorem:
(defthm cst-char-concs (implies (cst-list-list-alt-matchp abnf::cstss "unescaped / escape ( %x22 / %x5C / %x2F / %x62 / %x66 / %x6E / %x72 / %x74 / %x75 4hexdig )") (or (cst-list-list-conc-matchp abnf::cstss "unescaped") (cst-list-list-conc-matchp abnf::cstss "escape ( %x22 / %x5C / %x2F / %x62 / %x66 / %x6E / %x72 / %x74 / %x75 4hexdig )"))))
Theorem:
(defthm cst-escape-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x5C") (or (cst-list-list-conc-matchp abnf::cstss "%x5C"))))
Theorem:
(defthm cst-quotation-mark-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x22") (or (cst-list-list-conc-matchp abnf::cstss "%x22"))))
Theorem:
(defthm cst-unescaped-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x20-21 / %x23-5B / %x5D-10FFFF") (or (cst-list-list-conc-matchp abnf::cstss "%x20-21") (cst-list-list-conc-matchp abnf::cstss "%x23-5B") (cst-list-list-conc-matchp abnf::cstss "%x5D-10FFFF"))))
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-hexdig-concs (implies (cst-list-list-alt-matchp abnf::cstss "digit / \"A\" / \"B\" / \"C\" / \"D\" / \"E\" / \"F\"") (or (cst-list-list-conc-matchp abnf::cstss "digit") (cst-list-list-conc-matchp abnf::cstss "\"A\"") (cst-list-list-conc-matchp abnf::cstss "\"B\"") (cst-list-list-conc-matchp abnf::cstss "\"C\"") (cst-list-list-conc-matchp abnf::cstss "\"D\"") (cst-list-list-conc-matchp abnf::cstss "\"E\"") (cst-list-list-conc-matchp abnf::cstss "\"F\""))))
Theorem:
(defthm cst-ws-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "*( %x20 / %x9 / %xA / %xD )") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "*( %x20 / %x9 / %xA / %xD )"))))
Theorem:
(defthm cst-value-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "false") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "false"))))
Theorem:
(defthm cst-value-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "null") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "null"))))
Theorem:
(defthm cst-value-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "true") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "true"))))
Theorem:
(defthm cst-value-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "object") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "object"))))
Theorem:
(defthm cst-value-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "array") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "array"))))
Theorem:
(defthm cst-value-conc6-matching (implies (cst-list-list-conc-matchp abnf::cstss "number") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "number"))))
Theorem:
(defthm cst-value-conc7-matching (implies (cst-list-list-conc-matchp abnf::cstss "string") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "string"))))
Theorem:
(defthm cst-false-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x66.61.6C.73.65") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x66.61.6C.73.65"))))
Theorem:
(defthm cst-null-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x6E.75.6C.6C") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x6E.75.6C.6C"))))
Theorem:
(defthm cst-true-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x74.72.75.65") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x74.72.75.65"))))
Theorem:
(defthm cst-decimal-point-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x2E") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x2E"))))
Theorem:
(defthm cst-digit1-9-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x31-39") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x31-39"))))
Theorem:
(defthm cst-e-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x65") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x65"))))
Theorem:
(defthm cst-e-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x45") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x45"))))
Theorem:
(defthm cst-int-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "zero") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "zero"))))
Theorem:
(defthm cst-int-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "( digit1-9 *digit )") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "( digit1-9 *digit )"))))
Theorem:
(defthm cst-minus-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x2D") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x2D"))))
Theorem:
(defthm cst-plus-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x2B") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x2B"))))
Theorem:
(defthm cst-zero-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x30") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x30"))))
Theorem:
(defthm cst-char-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "unescaped") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "unescaped"))))
Theorem:
(defthm cst-escape-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x5C") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x5C"))))
Theorem:
(defthm cst-quotation-mark-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x22") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x22"))))
Theorem:
(defthm cst-unescaped-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x20-21") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x20-21"))))
Theorem:
(defthm cst-unescaped-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x23-5B") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x23-5B"))))
Theorem:
(defthm cst-unescaped-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x5D-10FFFF") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x5D-10FFFF"))))
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-hexdig-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "digit") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "digit"))))
Theorem:
(defthm cst-hexdig-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"A\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"A\""))))
Theorem:
(defthm cst-hexdig-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"B\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"B\""))))
Theorem:
(defthm cst-hexdig-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"C\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"C\""))))
Theorem:
(defthm cst-hexdig-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"D\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"D\""))))
Theorem:
(defthm cst-hexdig-conc6-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"E\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"E\""))))
Theorem:
(defthm cst-hexdig-conc7-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"F\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"F\""))))
Theorem:
(defthm cst-value-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "false") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "false"))))
Theorem:
(defthm cst-value-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "null") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "null"))))
Theorem:
(defthm cst-value-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "true") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "true"))))
Theorem:
(defthm cst-value-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "object") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "object"))))
Theorem:
(defthm cst-value-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "array") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "array"))))
Theorem:
(defthm cst-value-conc6-rep-matching (implies (cst-list-rep-matchp abnf::csts "number") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "number"))))
Theorem:
(defthm cst-value-conc7-rep-matching (implies (cst-list-rep-matchp abnf::csts "string") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "string"))))
Theorem:
(defthm cst-false-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x66.61.6C.73.65") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x66.61.6C.73.65"))))
Theorem:
(defthm cst-null-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x6E.75.6C.6C") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x6E.75.6C.6C"))))
Theorem:
(defthm cst-true-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x74.72.75.65") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x74.72.75.65"))))
Theorem:
(defthm cst-decimal-point-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x2E") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x2E"))))
Theorem:
(defthm cst-digit1-9-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x31-39") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x31-39"))))
Theorem:
(defthm cst-e-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x65") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x65"))))
Theorem:
(defthm cst-e-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x45") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x45"))))
Theorem:
(defthm cst-int-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "zero") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "zero"))))
Theorem:
(defthm cst-int-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "( digit1-9 *digit )") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "( digit1-9 *digit )"))))
Theorem:
(defthm cst-minus-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x2D") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x2D"))))
Theorem:
(defthm cst-plus-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x2B") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x2B"))))
Theorem:
(defthm cst-zero-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x30") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x30"))))
Theorem:
(defthm cst-char-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "unescaped") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "unescaped"))))
Theorem:
(defthm cst-escape-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x5C") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x5C"))))
Theorem:
(defthm cst-quotation-mark-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x22") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x22"))))
Theorem:
(defthm cst-unescaped-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x20-21") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x20-21"))))
Theorem:
(defthm cst-unescaped-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x23-5B") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x23-5B"))))
Theorem:
(defthm cst-unescaped-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x5D-10FFFF") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x5D-10FFFF"))))
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-hexdig-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "digit") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "digit"))))
Theorem:
(defthm cst-hexdig-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"A\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"A\""))))
Theorem:
(defthm cst-hexdig-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"B\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"B\""))))
Theorem:
(defthm cst-hexdig-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"C\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"C\""))))
Theorem:
(defthm cst-hexdig-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"D\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"D\""))))
Theorem:
(defthm cst-hexdig-conc6-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"E\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"E\""))))
Theorem:
(defthm cst-hexdig-conc7-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"F\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"F\""))))
Theorem:
(defthm cst-value-conc-equivs (implies (cst-matchp abnf::cst "value") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "false") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "false"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "null") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "null"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "true") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "true"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "object") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "object"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "array") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "array"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "number") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "number"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "string") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "string"))))))
Function:
(defun cst-value-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "value"))) (let ((__function__ 'cst-value-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "false")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "null")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "true")) 3) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "object")) 4) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "array")) 5) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "number")) 6) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "string")) 7) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-value-conc? (b* ((number (cst-value-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc?-possibilities (b* ((number (cst-value-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4) (equal number 5) (equal number 6) (equal number 7))) :rule-classes ((:forward-chaining :trigger-terms ((cst-value-conc? abnf::cst)))))
Theorem:
(defthm cst-value-conc?-of-tree-fix-cst (equal (cst-value-conc? (abnf::tree-fix abnf::cst)) (cst-value-conc? abnf::cst)))
Theorem:
(defthm cst-value-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc? abnf::cst) (cst-value-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-value-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "value") (iff (equal (cst-value-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "false"))))
Theorem:
(defthm cst-value-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "value") (iff (equal (cst-value-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "null"))))
Theorem:
(defthm cst-value-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "value") (iff (equal (cst-value-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "true"))))
Theorem:
(defthm cst-value-conc?-4-iff-match-conc (implies (cst-matchp abnf::cst "value") (iff (equal (cst-value-conc? abnf::cst) 4) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "object"))))
Theorem:
(defthm cst-value-conc?-5-iff-match-conc (implies (cst-matchp abnf::cst "value") (iff (equal (cst-value-conc? abnf::cst) 5) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "array"))))
Theorem:
(defthm cst-value-conc?-6-iff-match-conc (implies (cst-matchp abnf::cst "value") (iff (equal (cst-value-conc? abnf::cst) 6) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "number"))))
Theorem:
(defthm cst-value-conc?-7-iff-match-conc (implies (cst-matchp abnf::cst "value") (iff (equal (cst-value-conc? abnf::cst) 7) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "string"))))
Function:
(defun cst-json-text-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "json-text"))) (let ((__function__ 'cst-json-text-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-json-text-conc (b* ((abnf::cstss (cst-json-text-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-json-text-conc-match (implies (cst-matchp abnf::cst "json-text") (b* ((abnf::cstss (cst-json-text-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "ws value ws"))) :rule-classes :rewrite)
Theorem:
(defthm cst-json-text-conc-of-tree-fix-cst (equal (cst-json-text-conc (abnf::tree-fix abnf::cst)) (cst-json-text-conc abnf::cst)))
Theorem:
(defthm cst-json-text-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-json-text-conc abnf::cst) (cst-json-text-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-begin-array-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "begin-array"))) (let ((__function__ 'cst-begin-array-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-begin-array-conc (b* ((abnf::cstss (cst-begin-array-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-begin-array-conc-match (implies (cst-matchp abnf::cst "begin-array") (b* ((abnf::cstss (cst-begin-array-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "ws %x5B ws"))) :rule-classes :rewrite)
Theorem:
(defthm cst-begin-array-conc-of-tree-fix-cst (equal (cst-begin-array-conc (abnf::tree-fix abnf::cst)) (cst-begin-array-conc abnf::cst)))
Theorem:
(defthm cst-begin-array-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-begin-array-conc abnf::cst) (cst-begin-array-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-begin-object-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "begin-object"))) (let ((__function__ 'cst-begin-object-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-begin-object-conc (b* ((abnf::cstss (cst-begin-object-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-begin-object-conc-match (implies (cst-matchp abnf::cst "begin-object") (b* ((abnf::cstss (cst-begin-object-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "ws %x7B ws"))) :rule-classes :rewrite)
Theorem:
(defthm cst-begin-object-conc-of-tree-fix-cst (equal (cst-begin-object-conc (abnf::tree-fix abnf::cst)) (cst-begin-object-conc abnf::cst)))
Theorem:
(defthm cst-begin-object-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-begin-object-conc abnf::cst) (cst-begin-object-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-end-array-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "end-array"))) (let ((__function__ 'cst-end-array-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-end-array-conc (b* ((abnf::cstss (cst-end-array-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-end-array-conc-match (implies (cst-matchp abnf::cst "end-array") (b* ((abnf::cstss (cst-end-array-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "ws %x5D ws"))) :rule-classes :rewrite)
Theorem:
(defthm cst-end-array-conc-of-tree-fix-cst (equal (cst-end-array-conc (abnf::tree-fix abnf::cst)) (cst-end-array-conc abnf::cst)))
Theorem:
(defthm cst-end-array-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-end-array-conc abnf::cst) (cst-end-array-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-end-object-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "end-object"))) (let ((__function__ 'cst-end-object-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-end-object-conc (b* ((abnf::cstss (cst-end-object-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-end-object-conc-match (implies (cst-matchp abnf::cst "end-object") (b* ((abnf::cstss (cst-end-object-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "ws %x7D ws"))) :rule-classes :rewrite)
Theorem:
(defthm cst-end-object-conc-of-tree-fix-cst (equal (cst-end-object-conc (abnf::tree-fix abnf::cst)) (cst-end-object-conc abnf::cst)))
Theorem:
(defthm cst-end-object-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-end-object-conc abnf::cst) (cst-end-object-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-name-separator-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "name-separator"))) (let ((__function__ 'cst-name-separator-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-name-separator-conc (b* ((abnf::cstss (cst-name-separator-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-name-separator-conc-match (implies (cst-matchp abnf::cst "name-separator") (b* ((abnf::cstss (cst-name-separator-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "ws %x3A ws"))) :rule-classes :rewrite)
Theorem:
(defthm cst-name-separator-conc-of-tree-fix-cst (equal (cst-name-separator-conc (abnf::tree-fix abnf::cst)) (cst-name-separator-conc abnf::cst)))
Theorem:
(defthm cst-name-separator-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-name-separator-conc abnf::cst) (cst-name-separator-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-separator-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "value-separator"))) (let ((__function__ 'cst-value-separator-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-value-separator-conc (b* ((abnf::cstss (cst-value-separator-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-separator-conc-match (implies (cst-matchp abnf::cst "value-separator") (b* ((abnf::cstss (cst-value-separator-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "ws %x2C ws"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-separator-conc-of-tree-fix-cst (equal (cst-value-separator-conc (abnf::tree-fix abnf::cst)) (cst-value-separator-conc abnf::cst)))
Theorem:
(defthm cst-value-separator-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-separator-conc abnf::cst) (cst-value-separator-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-ws-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "ws"))) (let ((__function__ 'cst-ws-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-ws-conc (b* ((abnf::cstss (cst-ws-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-ws-conc-match (implies (cst-matchp abnf::cst "ws") (b* ((abnf::cstss (cst-ws-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "*( %x20 / %x9 / %xA / %xD )"))) :rule-classes :rewrite)
Theorem:
(defthm cst-ws-conc-of-tree-fix-cst (equal (cst-ws-conc (abnf::tree-fix abnf::cst)) (cst-ws-conc abnf::cst)))
Theorem:
(defthm cst-ws-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-ws-conc abnf::cst) (cst-ws-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 1)))) (let ((__function__ 'cst-value-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-value-conc1 (b* ((abnf::cstss (cst-value-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc1-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-value-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "false"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc1-of-tree-fix-cst (equal (cst-value-conc1 (abnf::tree-fix abnf::cst)) (cst-value-conc1 abnf::cst)))
Theorem:
(defthm cst-value-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc1 abnf::cst) (cst-value-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 2)))) (let ((__function__ 'cst-value-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-value-conc2 (b* ((abnf::cstss (cst-value-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc2-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-value-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "null"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc2-of-tree-fix-cst (equal (cst-value-conc2 (abnf::tree-fix abnf::cst)) (cst-value-conc2 abnf::cst)))
Theorem:
(defthm cst-value-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc2 abnf::cst) (cst-value-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc3 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 3)))) (let ((__function__ 'cst-value-conc3)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-value-conc3 (b* ((abnf::cstss (cst-value-conc3 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc3-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 3)) (b* ((abnf::cstss (cst-value-conc3 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "true"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc3-of-tree-fix-cst (equal (cst-value-conc3 (abnf::tree-fix abnf::cst)) (cst-value-conc3 abnf::cst)))
Theorem:
(defthm cst-value-conc3-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc3 abnf::cst) (cst-value-conc3 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc4 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 4)))) (let ((__function__ 'cst-value-conc4)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-value-conc4 (b* ((abnf::cstss (cst-value-conc4 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc4-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 4)) (b* ((abnf::cstss (cst-value-conc4 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "object"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc4-of-tree-fix-cst (equal (cst-value-conc4 (abnf::tree-fix abnf::cst)) (cst-value-conc4 abnf::cst)))
Theorem:
(defthm cst-value-conc4-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc4 abnf::cst) (cst-value-conc4 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc5 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 5)))) (let ((__function__ 'cst-value-conc5)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-value-conc5 (b* ((abnf::cstss (cst-value-conc5 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc5-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 5)) (b* ((abnf::cstss (cst-value-conc5 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "array"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc5-of-tree-fix-cst (equal (cst-value-conc5 (abnf::tree-fix abnf::cst)) (cst-value-conc5 abnf::cst)))
Theorem:
(defthm cst-value-conc5-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc5 abnf::cst) (cst-value-conc5 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc6 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 6)))) (let ((__function__ 'cst-value-conc6)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-value-conc6 (b* ((abnf::cstss (cst-value-conc6 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc6-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 6)) (b* ((abnf::cstss (cst-value-conc6 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc6-of-tree-fix-cst (equal (cst-value-conc6 (abnf::tree-fix abnf::cst)) (cst-value-conc6 abnf::cst)))
Theorem:
(defthm cst-value-conc6-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc6 abnf::cst) (cst-value-conc6 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc7 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 7)))) (let ((__function__ 'cst-value-conc7)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-value-conc7 (b* ((abnf::cstss (cst-value-conc7 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc7-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 7)) (b* ((abnf::cstss (cst-value-conc7 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "string"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc7-of-tree-fix-cst (equal (cst-value-conc7 (abnf::tree-fix abnf::cst)) (cst-value-conc7 abnf::cst)))
Theorem:
(defthm cst-value-conc7-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc7 abnf::cst) (cst-value-conc7 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-false-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "false"))) (let ((__function__ 'cst-false-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-false-conc (b* ((abnf::cstss (cst-false-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-false-conc-match (implies (cst-matchp abnf::cst "false") (b* ((abnf::cstss (cst-false-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x66.61.6C.73.65"))) :rule-classes :rewrite)
Theorem:
(defthm cst-false-conc-of-tree-fix-cst (equal (cst-false-conc (abnf::tree-fix abnf::cst)) (cst-false-conc abnf::cst)))
Theorem:
(defthm cst-false-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-false-conc abnf::cst) (cst-false-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-null-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "null"))) (let ((__function__ 'cst-null-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-null-conc (b* ((abnf::cstss (cst-null-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-null-conc-match (implies (cst-matchp abnf::cst "null") (b* ((abnf::cstss (cst-null-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x6E.75.6C.6C"))) :rule-classes :rewrite)
Theorem:
(defthm cst-null-conc-of-tree-fix-cst (equal (cst-null-conc (abnf::tree-fix abnf::cst)) (cst-null-conc abnf::cst)))
Theorem:
(defthm cst-null-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-null-conc abnf::cst) (cst-null-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-true-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "true"))) (let ((__function__ 'cst-true-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-true-conc (b* ((abnf::cstss (cst-true-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-true-conc-match (implies (cst-matchp abnf::cst "true") (b* ((abnf::cstss (cst-true-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x74.72.75.65"))) :rule-classes :rewrite)
Theorem:
(defthm cst-true-conc-of-tree-fix-cst (equal (cst-true-conc (abnf::tree-fix abnf::cst)) (cst-true-conc abnf::cst)))
Theorem:
(defthm cst-true-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-true-conc abnf::cst) (cst-true-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-object-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "object"))) (let ((__function__ 'cst-object-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-object-conc (b* ((abnf::cstss (cst-object-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-object-conc-match (implies (cst-matchp abnf::cst "object") (b* ((abnf::cstss (cst-object-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "begin-object [ member *( value-separator member ) ] end-object"))) :rule-classes :rewrite)
Theorem:
(defthm cst-object-conc-of-tree-fix-cst (equal (cst-object-conc (abnf::tree-fix abnf::cst)) (cst-object-conc abnf::cst)))
Theorem:
(defthm cst-object-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-object-conc abnf::cst) (cst-object-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-member-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "member"))) (let ((__function__ 'cst-member-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-member-conc (b* ((abnf::cstss (cst-member-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-member-conc-match (implies (cst-matchp abnf::cst "member") (b* ((abnf::cstss (cst-member-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "string name-separator value"))) :rule-classes :rewrite)
Theorem:
(defthm cst-member-conc-of-tree-fix-cst (equal (cst-member-conc (abnf::tree-fix abnf::cst)) (cst-member-conc abnf::cst)))
Theorem:
(defthm cst-member-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-member-conc abnf::cst) (cst-member-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-array-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "array"))) (let ((__function__ 'cst-array-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-array-conc (b* ((abnf::cstss (cst-array-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-array-conc-match (implies (cst-matchp abnf::cst "array") (b* ((abnf::cstss (cst-array-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "begin-array [ value *( value-separator value ) ] end-array"))) :rule-classes :rewrite)
Theorem:
(defthm cst-array-conc-of-tree-fix-cst (equal (cst-array-conc (abnf::tree-fix abnf::cst)) (cst-array-conc abnf::cst)))
Theorem:
(defthm cst-array-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-array-conc abnf::cst) (cst-array-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-number-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "number"))) (let ((__function__ 'cst-number-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-number-conc (b* ((abnf::cstss (cst-number-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-number-conc-match (implies (cst-matchp abnf::cst "number") (b* ((abnf::cstss (cst-number-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "[ minus ] int [ frac ] [ exp ]"))) :rule-classes :rewrite)
Theorem:
(defthm cst-number-conc-of-tree-fix-cst (equal (cst-number-conc (abnf::tree-fix abnf::cst)) (cst-number-conc abnf::cst)))
Theorem:
(defthm cst-number-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-number-conc abnf::cst) (cst-number-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-decimal-point-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "decimal-point"))) (let ((__function__ 'cst-decimal-point-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-decimal-point-conc (b* ((abnf::cstss (cst-decimal-point-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-point-conc-match (implies (cst-matchp abnf::cst "decimal-point") (b* ((abnf::cstss (cst-decimal-point-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x2E"))) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-point-conc-of-tree-fix-cst (equal (cst-decimal-point-conc (abnf::tree-fix abnf::cst)) (cst-decimal-point-conc abnf::cst)))
Theorem:
(defthm cst-decimal-point-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-decimal-point-conc abnf::cst) (cst-decimal-point-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-digit1-9-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "digit1-9"))) (let ((__function__ 'cst-digit1-9-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-digit1-9-conc (b* ((abnf::cstss (cst-digit1-9-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-digit1-9-conc-match (implies (cst-matchp abnf::cst "digit1-9") (b* ((abnf::cstss (cst-digit1-9-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x31-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-digit1-9-conc-of-tree-fix-cst (equal (cst-digit1-9-conc (abnf::tree-fix abnf::cst)) (cst-digit1-9-conc abnf::cst)))
Theorem:
(defthm cst-digit1-9-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-digit1-9-conc abnf::cst) (cst-digit1-9-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-exp-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "exp"))) (let ((__function__ 'cst-exp-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-exp-conc (b* ((abnf::cstss (cst-exp-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-exp-conc-match (implies (cst-matchp abnf::cst "exp") (b* ((abnf::cstss (cst-exp-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "e [ minus / plus ] 1*digit"))) :rule-classes :rewrite)
Theorem:
(defthm cst-exp-conc-of-tree-fix-cst (equal (cst-exp-conc (abnf::tree-fix abnf::cst)) (cst-exp-conc abnf::cst)))
Theorem:
(defthm cst-exp-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-exp-conc abnf::cst) (cst-exp-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-frac-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "frac"))) (let ((__function__ 'cst-frac-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-frac-conc (b* ((abnf::cstss (cst-frac-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-frac-conc-match (implies (cst-matchp abnf::cst "frac") (b* ((abnf::cstss (cst-frac-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "decimal-point 1*digit"))) :rule-classes :rewrite)
Theorem:
(defthm cst-frac-conc-of-tree-fix-cst (equal (cst-frac-conc (abnf::tree-fix abnf::cst)) (cst-frac-conc abnf::cst)))
Theorem:
(defthm cst-frac-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-frac-conc abnf::cst) (cst-frac-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-minus-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "minus"))) (let ((__function__ 'cst-minus-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-minus-conc (b* ((abnf::cstss (cst-minus-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-minus-conc-match (implies (cst-matchp abnf::cst "minus") (b* ((abnf::cstss (cst-minus-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x2D"))) :rule-classes :rewrite)
Theorem:
(defthm cst-minus-conc-of-tree-fix-cst (equal (cst-minus-conc (abnf::tree-fix abnf::cst)) (cst-minus-conc abnf::cst)))
Theorem:
(defthm cst-minus-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-minus-conc abnf::cst) (cst-minus-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-plus-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "plus"))) (let ((__function__ 'cst-plus-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-plus-conc (b* ((abnf::cstss (cst-plus-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-plus-conc-match (implies (cst-matchp abnf::cst "plus") (b* ((abnf::cstss (cst-plus-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x2B"))) :rule-classes :rewrite)
Theorem:
(defthm cst-plus-conc-of-tree-fix-cst (equal (cst-plus-conc (abnf::tree-fix abnf::cst)) (cst-plus-conc abnf::cst)))
Theorem:
(defthm cst-plus-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-plus-conc abnf::cst) (cst-plus-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-zero-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "zero"))) (let ((__function__ 'cst-zero-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-zero-conc (b* ((abnf::cstss (cst-zero-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-zero-conc-match (implies (cst-matchp abnf::cst "zero") (b* ((abnf::cstss (cst-zero-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x30"))) :rule-classes :rewrite)
Theorem:
(defthm cst-zero-conc-of-tree-fix-cst (equal (cst-zero-conc (abnf::tree-fix abnf::cst)) (cst-zero-conc abnf::cst)))
Theorem:
(defthm cst-zero-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-zero-conc abnf::cst) (cst-zero-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-string-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "string"))) (let ((__function__ 'cst-string-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-string-conc (b* ((abnf::cstss (cst-string-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-string-conc-match (implies (cst-matchp abnf::cst "string") (b* ((abnf::cstss (cst-string-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "quotation-mark *char quotation-mark"))) :rule-classes :rewrite)
Theorem:
(defthm cst-string-conc-of-tree-fix-cst (equal (cst-string-conc (abnf::tree-fix abnf::cst)) (cst-string-conc abnf::cst)))
Theorem:
(defthm cst-string-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-string-conc abnf::cst) (cst-string-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-escape-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "escape"))) (let ((__function__ 'cst-escape-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-escape-conc (b* ((abnf::cstss (cst-escape-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-escape-conc-match (implies (cst-matchp abnf::cst "escape") (b* ((abnf::cstss (cst-escape-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x5C"))) :rule-classes :rewrite)
Theorem:
(defthm cst-escape-conc-of-tree-fix-cst (equal (cst-escape-conc (abnf::tree-fix abnf::cst)) (cst-escape-conc abnf::cst)))
Theorem:
(defthm cst-escape-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-escape-conc abnf::cst) (cst-escape-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-quotation-mark-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "quotation-mark"))) (let ((__function__ 'cst-quotation-mark-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-quotation-mark-conc (b* ((abnf::cstss (cst-quotation-mark-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-quotation-mark-conc-match (implies (cst-matchp abnf::cst "quotation-mark") (b* ((abnf::cstss (cst-quotation-mark-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x22"))) :rule-classes :rewrite)
Theorem:
(defthm cst-quotation-mark-conc-of-tree-fix-cst (equal (cst-quotation-mark-conc (abnf::tree-fix abnf::cst)) (cst-quotation-mark-conc abnf::cst)))
Theorem:
(defthm cst-quotation-mark-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-quotation-mark-conc abnf::cst) (cst-quotation-mark-conc 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-value-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 1)))) (let ((__function__ 'cst-value-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-value-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-value-conc1-rep (b* ((abnf::csts (cst-value-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc1-rep-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-value-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "false"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc1-rep-of-tree-fix-cst (equal (cst-value-conc1-rep (abnf::tree-fix abnf::cst)) (cst-value-conc1-rep abnf::cst)))
Theorem:
(defthm cst-value-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc1-rep abnf::cst) (cst-value-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 2)))) (let ((__function__ 'cst-value-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-value-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-value-conc2-rep (b* ((abnf::csts (cst-value-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc2-rep-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-value-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "null"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc2-rep-of-tree-fix-cst (equal (cst-value-conc2-rep (abnf::tree-fix abnf::cst)) (cst-value-conc2-rep abnf::cst)))
Theorem:
(defthm cst-value-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc2-rep abnf::cst) (cst-value-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc3-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 3)))) (let ((__function__ 'cst-value-conc3-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-value-conc3 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-value-conc3-rep (b* ((abnf::csts (cst-value-conc3-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc3-rep-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 3)) (b* ((abnf::csts (cst-value-conc3-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "true"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc3-rep-of-tree-fix-cst (equal (cst-value-conc3-rep (abnf::tree-fix abnf::cst)) (cst-value-conc3-rep abnf::cst)))
Theorem:
(defthm cst-value-conc3-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc3-rep abnf::cst) (cst-value-conc3-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc4-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 4)))) (let ((__function__ 'cst-value-conc4-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-value-conc4 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-value-conc4-rep (b* ((abnf::csts (cst-value-conc4-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc4-rep-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 4)) (b* ((abnf::csts (cst-value-conc4-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "object"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc4-rep-of-tree-fix-cst (equal (cst-value-conc4-rep (abnf::tree-fix abnf::cst)) (cst-value-conc4-rep abnf::cst)))
Theorem:
(defthm cst-value-conc4-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc4-rep abnf::cst) (cst-value-conc4-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc5-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 5)))) (let ((__function__ 'cst-value-conc5-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-value-conc5 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-value-conc5-rep (b* ((abnf::csts (cst-value-conc5-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc5-rep-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 5)) (b* ((abnf::csts (cst-value-conc5-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "array"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc5-rep-of-tree-fix-cst (equal (cst-value-conc5-rep (abnf::tree-fix abnf::cst)) (cst-value-conc5-rep abnf::cst)))
Theorem:
(defthm cst-value-conc5-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc5-rep abnf::cst) (cst-value-conc5-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc6-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 6)))) (let ((__function__ 'cst-value-conc6-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-value-conc6 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-value-conc6-rep (b* ((abnf::csts (cst-value-conc6-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc6-rep-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 6)) (b* ((abnf::csts (cst-value-conc6-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc6-rep-of-tree-fix-cst (equal (cst-value-conc6-rep (abnf::tree-fix abnf::cst)) (cst-value-conc6-rep abnf::cst)))
Theorem:
(defthm cst-value-conc6-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc6-rep abnf::cst) (cst-value-conc6-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc7-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 7)))) (let ((__function__ 'cst-value-conc7-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-value-conc7 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-value-conc7-rep (b* ((abnf::csts (cst-value-conc7-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc7-rep-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 7)) (b* ((abnf::csts (cst-value-conc7-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "string"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc7-rep-of-tree-fix-cst (equal (cst-value-conc7-rep (abnf::tree-fix abnf::cst)) (cst-value-conc7-rep abnf::cst)))
Theorem:
(defthm cst-value-conc7-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc7-rep abnf::cst) (cst-value-conc7-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-false-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "false"))) (let ((__function__ 'cst-false-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-false-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-false-conc-rep (b* ((abnf::csts (cst-false-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-false-conc-rep-match (implies (cst-matchp abnf::cst "false") (b* ((abnf::csts (cst-false-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x66.61.6C.73.65"))) :rule-classes :rewrite)
Theorem:
(defthm cst-false-conc-rep-of-tree-fix-cst (equal (cst-false-conc-rep (abnf::tree-fix abnf::cst)) (cst-false-conc-rep abnf::cst)))
Theorem:
(defthm cst-false-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-false-conc-rep abnf::cst) (cst-false-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-null-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "null"))) (let ((__function__ 'cst-null-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-null-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-null-conc-rep (b* ((abnf::csts (cst-null-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-null-conc-rep-match (implies (cst-matchp abnf::cst "null") (b* ((abnf::csts (cst-null-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x6E.75.6C.6C"))) :rule-classes :rewrite)
Theorem:
(defthm cst-null-conc-rep-of-tree-fix-cst (equal (cst-null-conc-rep (abnf::tree-fix abnf::cst)) (cst-null-conc-rep abnf::cst)))
Theorem:
(defthm cst-null-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-null-conc-rep abnf::cst) (cst-null-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-true-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "true"))) (let ((__function__ 'cst-true-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-true-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-true-conc-rep (b* ((abnf::csts (cst-true-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-true-conc-rep-match (implies (cst-matchp abnf::cst "true") (b* ((abnf::csts (cst-true-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x74.72.75.65"))) :rule-classes :rewrite)
Theorem:
(defthm cst-true-conc-rep-of-tree-fix-cst (equal (cst-true-conc-rep (abnf::tree-fix abnf::cst)) (cst-true-conc-rep abnf::cst)))
Theorem:
(defthm cst-true-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-true-conc-rep abnf::cst) (cst-true-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-decimal-point-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "decimal-point"))) (let ((__function__ 'cst-decimal-point-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-decimal-point-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-decimal-point-conc-rep (b* ((abnf::csts (cst-decimal-point-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-point-conc-rep-match (implies (cst-matchp abnf::cst "decimal-point") (b* ((abnf::csts (cst-decimal-point-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x2E"))) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-point-conc-rep-of-tree-fix-cst (equal (cst-decimal-point-conc-rep (abnf::tree-fix abnf::cst)) (cst-decimal-point-conc-rep abnf::cst)))
Theorem:
(defthm cst-decimal-point-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-decimal-point-conc-rep abnf::cst) (cst-decimal-point-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-digit1-9-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "digit1-9"))) (let ((__function__ 'cst-digit1-9-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-digit1-9-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-digit1-9-conc-rep (b* ((abnf::csts (cst-digit1-9-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-digit1-9-conc-rep-match (implies (cst-matchp abnf::cst "digit1-9") (b* ((abnf::csts (cst-digit1-9-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x31-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-digit1-9-conc-rep-of-tree-fix-cst (equal (cst-digit1-9-conc-rep (abnf::tree-fix abnf::cst)) (cst-digit1-9-conc-rep abnf::cst)))
Theorem:
(defthm cst-digit1-9-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-digit1-9-conc-rep abnf::cst) (cst-digit1-9-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-minus-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "minus"))) (let ((__function__ 'cst-minus-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-minus-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-minus-conc-rep (b* ((abnf::csts (cst-minus-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-minus-conc-rep-match (implies (cst-matchp abnf::cst "minus") (b* ((abnf::csts (cst-minus-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x2D"))) :rule-classes :rewrite)
Theorem:
(defthm cst-minus-conc-rep-of-tree-fix-cst (equal (cst-minus-conc-rep (abnf::tree-fix abnf::cst)) (cst-minus-conc-rep abnf::cst)))
Theorem:
(defthm cst-minus-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-minus-conc-rep abnf::cst) (cst-minus-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-plus-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "plus"))) (let ((__function__ 'cst-plus-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-plus-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-plus-conc-rep (b* ((abnf::csts (cst-plus-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-plus-conc-rep-match (implies (cst-matchp abnf::cst "plus") (b* ((abnf::csts (cst-plus-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x2B"))) :rule-classes :rewrite)
Theorem:
(defthm cst-plus-conc-rep-of-tree-fix-cst (equal (cst-plus-conc-rep (abnf::tree-fix abnf::cst)) (cst-plus-conc-rep abnf::cst)))
Theorem:
(defthm cst-plus-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-plus-conc-rep abnf::cst) (cst-plus-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-zero-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "zero"))) (let ((__function__ 'cst-zero-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-zero-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-zero-conc-rep (b* ((abnf::csts (cst-zero-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-zero-conc-rep-match (implies (cst-matchp abnf::cst "zero") (b* ((abnf::csts (cst-zero-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x30"))) :rule-classes :rewrite)
Theorem:
(defthm cst-zero-conc-rep-of-tree-fix-cst (equal (cst-zero-conc-rep (abnf::tree-fix abnf::cst)) (cst-zero-conc-rep abnf::cst)))
Theorem:
(defthm cst-zero-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-zero-conc-rep abnf::cst) (cst-zero-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-escape-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "escape"))) (let ((__function__ 'cst-escape-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-escape-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-escape-conc-rep (b* ((abnf::csts (cst-escape-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-escape-conc-rep-match (implies (cst-matchp abnf::cst "escape") (b* ((abnf::csts (cst-escape-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x5C"))) :rule-classes :rewrite)
Theorem:
(defthm cst-escape-conc-rep-of-tree-fix-cst (equal (cst-escape-conc-rep (abnf::tree-fix abnf::cst)) (cst-escape-conc-rep abnf::cst)))
Theorem:
(defthm cst-escape-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-escape-conc-rep abnf::cst) (cst-escape-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-quotation-mark-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "quotation-mark"))) (let ((__function__ 'cst-quotation-mark-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-quotation-mark-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-quotation-mark-conc-rep (b* ((abnf::csts (cst-quotation-mark-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-quotation-mark-conc-rep-match (implies (cst-matchp abnf::cst "quotation-mark") (b* ((abnf::csts (cst-quotation-mark-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x22"))) :rule-classes :rewrite)
Theorem:
(defthm cst-quotation-mark-conc-rep-of-tree-fix-cst (equal (cst-quotation-mark-conc-rep (abnf::tree-fix abnf::cst)) (cst-quotation-mark-conc-rep abnf::cst)))
Theorem:
(defthm cst-quotation-mark-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-quotation-mark-conc-rep abnf::cst) (cst-quotation-mark-conc-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-value-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 1)))) (let ((__function__ 'cst-value-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-value-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-value-conc1-rep-elem (b* ((abnf::cst1 (cst-value-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-value-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "false"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc1-rep-elem-of-tree-fix-cst (equal (cst-value-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-value-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-value-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc1-rep-elem abnf::cst) (cst-value-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 2)))) (let ((__function__ 'cst-value-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-value-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-value-conc2-rep-elem (b* ((abnf::cst1 (cst-value-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-value-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "null"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc2-rep-elem-of-tree-fix-cst (equal (cst-value-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-value-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-value-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc2-rep-elem abnf::cst) (cst-value-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc3-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 3)))) (let ((__function__ 'cst-value-conc3-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-value-conc3-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-value-conc3-rep-elem (b* ((abnf::cst1 (cst-value-conc3-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc3-rep-elem-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 3)) (b* ((abnf::cst1 (cst-value-conc3-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "true"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc3-rep-elem-of-tree-fix-cst (equal (cst-value-conc3-rep-elem (abnf::tree-fix abnf::cst)) (cst-value-conc3-rep-elem abnf::cst)))
Theorem:
(defthm cst-value-conc3-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc3-rep-elem abnf::cst) (cst-value-conc3-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc4-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 4)))) (let ((__function__ 'cst-value-conc4-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-value-conc4-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-value-conc4-rep-elem (b* ((abnf::cst1 (cst-value-conc4-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc4-rep-elem-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 4)) (b* ((abnf::cst1 (cst-value-conc4-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "object"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc4-rep-elem-of-tree-fix-cst (equal (cst-value-conc4-rep-elem (abnf::tree-fix abnf::cst)) (cst-value-conc4-rep-elem abnf::cst)))
Theorem:
(defthm cst-value-conc4-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc4-rep-elem abnf::cst) (cst-value-conc4-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc5-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 5)))) (let ((__function__ 'cst-value-conc5-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-value-conc5-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-value-conc5-rep-elem (b* ((abnf::cst1 (cst-value-conc5-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc5-rep-elem-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 5)) (b* ((abnf::cst1 (cst-value-conc5-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "array"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc5-rep-elem-of-tree-fix-cst (equal (cst-value-conc5-rep-elem (abnf::tree-fix abnf::cst)) (cst-value-conc5-rep-elem abnf::cst)))
Theorem:
(defthm cst-value-conc5-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc5-rep-elem abnf::cst) (cst-value-conc5-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc6-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 6)))) (let ((__function__ 'cst-value-conc6-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-value-conc6-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-value-conc6-rep-elem (b* ((abnf::cst1 (cst-value-conc6-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc6-rep-elem-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 6)) (b* ((abnf::cst1 (cst-value-conc6-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc6-rep-elem-of-tree-fix-cst (equal (cst-value-conc6-rep-elem (abnf::tree-fix abnf::cst)) (cst-value-conc6-rep-elem abnf::cst)))
Theorem:
(defthm cst-value-conc6-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc6-rep-elem abnf::cst) (cst-value-conc6-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-value-conc7-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 7)))) (let ((__function__ 'cst-value-conc7-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-value-conc7-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-value-conc7-rep-elem (b* ((abnf::cst1 (cst-value-conc7-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc7-rep-elem-match (implies (and (cst-matchp abnf::cst "value") (equal (cst-value-conc? abnf::cst) 7)) (b* ((abnf::cst1 (cst-value-conc7-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "string"))) :rule-classes :rewrite)
Theorem:
(defthm cst-value-conc7-rep-elem-of-tree-fix-cst (equal (cst-value-conc7-rep-elem (abnf::tree-fix abnf::cst)) (cst-value-conc7-rep-elem abnf::cst)))
Theorem:
(defthm cst-value-conc7-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-value-conc7-rep-elem abnf::cst) (cst-value-conc7-rep-elem cst-equiv))) :rule-classes :congruence)