Tree operations specialized to *grammar-new*.
Function:
(defun cst-matchp$ (abnf::tree abnf::elem) (declare (xargs :guard (and (abnf::treep abnf::tree) (abnf::elementp abnf::elem)))) (let ((__function__ 'cst-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-terminatedp abnf::tree) (abnf::tree-match-element-p abnf::tree abnf::elem *grammar-new*))))
Theorem:
(defthm booleanp-of-cst-matchp$ (b* ((abnf::yes/no (cst-matchp$ abnf::tree abnf::elem))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-matchp$-of-tree-fix-tree (equal (cst-matchp$ (abnf::tree-fix abnf::tree) abnf::elem) (cst-matchp$ abnf::tree abnf::elem)))
Theorem:
(defthm cst-matchp$-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv abnf::tree tree-equiv) (equal (cst-matchp$ abnf::tree abnf::elem) (cst-matchp$ tree-equiv abnf::elem))) :rule-classes :congruence)
Theorem:
(defthm cst-matchp$-of-element-fix-elem (equal (cst-matchp$ abnf::tree (abnf::element-fix abnf::elem)) (cst-matchp$ abnf::tree abnf::elem)))
Theorem:
(defthm cst-matchp$-element-equiv-congruence-on-elem (implies (abnf::element-equiv abnf::elem elem-equiv) (equal (cst-matchp$ abnf::tree abnf::elem) (cst-matchp$ abnf::tree elem-equiv))) :rule-classes :congruence)
Function:
(defun cst-list-elem-matchp$ (abnf::trees abnf::elem) (declare (xargs :guard (and (abnf::tree-listp abnf::trees) (abnf::elementp abnf::elem)))) (let ((__function__ 'cst-list-elem-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-list-terminatedp abnf::trees) (abnf::tree-list-match-element-p abnf::trees abnf::elem *grammar-new*))))
Theorem:
(defthm booleanp-of-cst-list-elem-matchp$ (b* ((abnf::yes/no (cst-list-elem-matchp$ abnf::trees abnf::elem))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-list-elem-matchp$-of-tree-list-fix-trees (equal (cst-list-elem-matchp$ (abnf::tree-list-fix abnf::trees) abnf::elem) (cst-list-elem-matchp$ abnf::trees abnf::elem)))
Theorem:
(defthm cst-list-elem-matchp$-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv abnf::trees trees-equiv) (equal (cst-list-elem-matchp$ abnf::trees abnf::elem) (cst-list-elem-matchp$ trees-equiv abnf::elem))) :rule-classes :congruence)
Theorem:
(defthm cst-list-elem-matchp$-of-element-fix-elem (equal (cst-list-elem-matchp$ abnf::trees (abnf::element-fix abnf::elem)) (cst-list-elem-matchp$ abnf::trees abnf::elem)))
Theorem:
(defthm cst-list-elem-matchp$-element-equiv-congruence-on-elem (implies (abnf::element-equiv abnf::elem elem-equiv) (equal (cst-list-elem-matchp$ abnf::trees abnf::elem) (cst-list-elem-matchp$ abnf::trees elem-equiv))) :rule-classes :congruence)
Function:
(defun cst-list-rep-matchp$ (abnf::trees abnf::rep) (declare (xargs :guard (and (abnf::tree-listp abnf::trees) (abnf::repetitionp abnf::rep)))) (let ((__function__ 'cst-list-rep-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-list-terminatedp abnf::trees) (abnf::tree-list-match-repetition-p abnf::trees abnf::rep *grammar-new*))))
Theorem:
(defthm booleanp-of-cst-list-rep-matchp$ (b* ((abnf::yes/no (cst-list-rep-matchp$ abnf::trees abnf::rep))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-list-rep-matchp$-of-tree-list-fix-trees (equal (cst-list-rep-matchp$ (abnf::tree-list-fix abnf::trees) abnf::rep) (cst-list-rep-matchp$ abnf::trees abnf::rep)))
Theorem:
(defthm cst-list-rep-matchp$-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv abnf::trees trees-equiv) (equal (cst-list-rep-matchp$ abnf::trees abnf::rep) (cst-list-rep-matchp$ trees-equiv abnf::rep))) :rule-classes :congruence)
Theorem:
(defthm cst-list-rep-matchp$-of-repetition-fix-rep (equal (cst-list-rep-matchp$ abnf::trees (abnf::repetition-fix abnf::rep)) (cst-list-rep-matchp$ abnf::trees abnf::rep)))
Theorem:
(defthm cst-list-rep-matchp$-repetition-equiv-congruence-on-rep (implies (abnf::repetition-equiv abnf::rep rep-equiv) (equal (cst-list-rep-matchp$ abnf::trees abnf::rep) (cst-list-rep-matchp$ abnf::trees rep-equiv))) :rule-classes :congruence)
Function:
(defun cst-list-list-conc-matchp$ (abnf::treess abnf::conc) (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess) (abnf::concatenationp abnf::conc)))) (let ((__function__ 'cst-list-list-conc-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-list-list-terminatedp abnf::treess) (abnf::tree-list-list-match-concatenation-p abnf::treess abnf::conc *grammar-new*))))
Theorem:
(defthm booleanp-of-cst-list-list-conc-matchp$ (b* ((abnf::yes/no (cst-list-list-conc-matchp$ abnf::treess abnf::conc))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-list-list-conc-matchp$-of-tree-list-list-fix-treess (equal (cst-list-list-conc-matchp$ (abnf::tree-list-list-fix abnf::treess) abnf::conc) (cst-list-list-conc-matchp$ abnf::treess abnf::conc)))
Theorem:
(defthm cst-list-list-conc-matchp$-tree-list-list-equiv-congruence-on-treess (implies (abnf::tree-list-list-equiv abnf::treess treess-equiv) (equal (cst-list-list-conc-matchp$ abnf::treess abnf::conc) (cst-list-list-conc-matchp$ treess-equiv abnf::conc))) :rule-classes :congruence)
Theorem:
(defthm cst-list-list-conc-matchp$-of-concatenation-fix-conc (equal (cst-list-list-conc-matchp$ abnf::treess (abnf::concatenation-fix abnf::conc)) (cst-list-list-conc-matchp$ abnf::treess abnf::conc)))
Theorem:
(defthm cst-list-list-conc-matchp$-concatenation-equiv-congruence-on-conc (implies (abnf::concatenation-equiv abnf::conc conc-equiv) (equal (cst-list-list-conc-matchp$ abnf::treess abnf::conc) (cst-list-list-conc-matchp$ abnf::treess conc-equiv))) :rule-classes :congruence)
Function:
(defun cst-list-list-alt-matchp$ (abnf::treess abnf::alt) (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess) (abnf::alternationp abnf::alt)))) (let ((__function__ 'cst-list-list-alt-matchp$)) (declare (ignorable __function__)) (and (abnf::tree-list-list-terminatedp abnf::treess) (abnf::tree-list-list-match-alternation-p abnf::treess abnf::alt *grammar-new*))))
Theorem:
(defthm booleanp-of-cst-list-list-alt-matchp$ (b* ((abnf::yes/no (cst-list-list-alt-matchp$ abnf::treess abnf::alt))) (booleanp abnf::yes/no)) :rule-classes :rewrite)
Theorem:
(defthm cst-list-list-alt-matchp$-of-tree-list-list-fix-treess (equal (cst-list-list-alt-matchp$ (abnf::tree-list-list-fix abnf::treess) abnf::alt) (cst-list-list-alt-matchp$ abnf::treess abnf::alt)))
Theorem:
(defthm cst-list-list-alt-matchp$-tree-list-list-equiv-congruence-on-treess (implies (abnf::tree-list-list-equiv abnf::treess treess-equiv) (equal (cst-list-list-alt-matchp$ abnf::treess abnf::alt) (cst-list-list-alt-matchp$ treess-equiv abnf::alt))) :rule-classes :congruence)
Theorem:
(defthm cst-list-list-alt-matchp$-of-alternation-fix-alt (equal (cst-list-list-alt-matchp$ abnf::treess (abnf::alternation-fix abnf::alt)) (cst-list-list-alt-matchp$ abnf::treess abnf::alt)))
Theorem:
(defthm cst-list-list-alt-matchp$-alternation-equiv-congruence-on-alt (implies (abnf::alternation-equiv abnf::alt alt-equiv) (equal (cst-list-list-alt-matchp$ abnf::treess abnf::alt) (cst-list-list-alt-matchp$ abnf::treess alt-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x0-9-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x0-9"))) (let ((__function__ 'cst-%x0-9-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x0-9-nat (b* ((nat (cst-%x0-9-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x0-9-nat-of-tree-fix-cst (equal (cst-%x0-9-nat (abnf::tree-fix abnf::cst)) (cst-%x0-9-nat abnf::cst)))
Theorem:
(defthm cst-%x0-9-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x0-9-nat abnf::cst) (cst-%x0-9-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x0-29-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x0-29"))) (let ((__function__ 'cst-%x0-29-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x0-29-nat (b* ((nat (cst-%x0-29-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x0-29-nat-of-tree-fix-cst (equal (cst-%x0-29-nat (abnf::tree-fix abnf::cst)) (cst-%x0-29-nat abnf::cst)))
Theorem:
(defthm cst-%x0-29-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x0-29-nat abnf::cst) (cst-%x0-29-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%xb-c-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%xB-C"))) (let ((__function__ 'cst-%xb-c-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%xb-c-nat (b* ((nat (cst-%xb-c-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%xb-c-nat-of-tree-fix-cst (equal (cst-%xb-c-nat (abnf::tree-fix abnf::cst)) (cst-%xb-c-nat abnf::cst)))
Theorem:
(defthm cst-%xb-c-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%xb-c-nat abnf::cst) (cst-%xb-c-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%xe-7f-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%xE-7F"))) (let ((__function__ 'cst-%xe-7f-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%xe-7f-nat (b* ((nat (cst-%xe-7f-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%xe-7f-nat-of-tree-fix-cst (equal (cst-%xe-7f-nat (abnf::tree-fix abnf::cst)) (cst-%xe-7f-nat abnf::cst)))
Theorem:
(defthm cst-%xe-7f-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%xe-7f-nat abnf::cst) (cst-%xe-7f-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x20-21-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x20-21"))) (let ((__function__ 'cst-%x20-21-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x20-21-nat (b* ((nat (cst-%x20-21-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x20-21-nat-of-tree-fix-cst (equal (cst-%x20-21-nat (abnf::tree-fix abnf::cst)) (cst-%x20-21-nat abnf::cst)))
Theorem:
(defthm cst-%x20-21-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x20-21-nat abnf::cst) (cst-%x20-21-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x20-26-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x20-26"))) (let ((__function__ 'cst-%x20-26-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x20-26-nat (b* ((nat (cst-%x20-26-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x20-26-nat-of-tree-fix-cst (equal (cst-%x20-26-nat (abnf::tree-fix abnf::cst)) (cst-%x20-26-nat abnf::cst)))
Theorem:
(defthm cst-%x20-26-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x20-26-nat abnf::cst) (cst-%x20-26-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x23-5b-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x23-5B"))) (let ((__function__ 'cst-%x23-5b-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x23-5b-nat (b* ((nat (cst-%x23-5b-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x23-5b-nat-of-tree-fix-cst (equal (cst-%x23-5b-nat (abnf::tree-fix abnf::cst)) (cst-%x23-5b-nat abnf::cst)))
Theorem:
(defthm cst-%x23-5b-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x23-5b-nat abnf::cst) (cst-%x23-5b-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x28-5b-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x28-5B"))) (let ((__function__ 'cst-%x28-5b-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x28-5b-nat (b* ((nat (cst-%x28-5b-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x28-5b-nat-of-tree-fix-cst (equal (cst-%x28-5b-nat (abnf::tree-fix abnf::cst)) (cst-%x28-5b-nat abnf::cst)))
Theorem:
(defthm cst-%x28-5b-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x28-5b-nat abnf::cst) (cst-%x28-5b-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x2b-2e-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x2B-2E"))) (let ((__function__ 'cst-%x2b-2e-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x2b-2e-nat (b* ((nat (cst-%x2b-2e-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x2b-2e-nat-of-tree-fix-cst (equal (cst-%x2b-2e-nat (abnf::tree-fix abnf::cst)) (cst-%x2b-2e-nat abnf::cst)))
Theorem:
(defthm cst-%x2b-2e-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x2b-2e-nat abnf::cst) (cst-%x2b-2e-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x2b-7f-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x2B-7F"))) (let ((__function__ 'cst-%x2b-7f-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x2b-7f-nat (b* ((nat (cst-%x2b-7f-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x2b-7f-nat-of-tree-fix-cst (equal (cst-%x2b-7f-nat (abnf::tree-fix abnf::cst)) (cst-%x2b-7f-nat abnf::cst)))
Theorem:
(defthm cst-%x2b-7f-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x2b-7f-nat abnf::cst) (cst-%x2b-7f-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x30-39-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x30-39"))) (let ((__function__ 'cst-%x30-39-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x30-39-nat (b* ((nat (cst-%x30-39-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x30-39-nat-of-tree-fix-cst (equal (cst-%x30-39-nat (abnf::tree-fix abnf::cst)) (cst-%x30-39-nat abnf::cst)))
Theorem:
(defthm cst-%x30-39-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x30-39-nat abnf::cst) (cst-%x30-39-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x30-7f-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x30-7F"))) (let ((__function__ 'cst-%x30-7f-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x30-7f-nat (b* ((nat (cst-%x30-7f-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x30-7f-nat-of-tree-fix-cst (equal (cst-%x30-7f-nat (abnf::tree-fix abnf::cst)) (cst-%x30-7f-nat abnf::cst)))
Theorem:
(defthm cst-%x30-7f-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x30-7f-nat abnf::cst) (cst-%x30-7f-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x31-39-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x31-39"))) (let ((__function__ 'cst-%x31-39-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x31-39-nat (b* ((nat (cst-%x31-39-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x31-39-nat-of-tree-fix-cst (equal (cst-%x31-39-nat (abnf::tree-fix abnf::cst)) (cst-%x31-39-nat abnf::cst)))
Theorem:
(defthm cst-%x31-39-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x31-39-nat abnf::cst) (cst-%x31-39-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x41-5a-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x41-5A"))) (let ((__function__ 'cst-%x41-5a-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x41-5a-nat (b* ((nat (cst-%x41-5a-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x41-5a-nat-of-tree-fix-cst (equal (cst-%x41-5a-nat (abnf::tree-fix abnf::cst)) (cst-%x41-5a-nat abnf::cst)))
Theorem:
(defthm cst-%x41-5a-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x41-5a-nat abnf::cst) (cst-%x41-5a-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x5d-7e-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x5D-7E"))) (let ((__function__ 'cst-%x5d-7e-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x5d-7e-nat (b* ((nat (cst-%x5d-7e-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x5d-7e-nat-of-tree-fix-cst (equal (cst-%x5d-7e-nat (abnf::tree-fix abnf::cst)) (cst-%x5d-7e-nat abnf::cst)))
Theorem:
(defthm cst-%x5d-7e-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x5d-7e-nat abnf::cst) (cst-%x5d-7e-nat cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-%x61-7a-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x61-7A"))) (let ((__function__ 'cst-%x61-7a-nat)) (declare (ignorable __function__)) (acl2::lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x61-7a-nat (b* ((nat (cst-%x61-7a-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x61-7a-nat-of-tree-fix-cst (equal (cst-%x61-7a-nat (abnf::tree-fix abnf::cst)) (cst-%x61-7a-nat abnf::cst)))
Theorem:
(defthm cst-%x61-7a-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x61-7a-nat abnf::cst) (cst-%x61-7a-nat cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-%x0-9-nat-bounds (implies (cst-matchp abnf::cst "%x0-9") (and (<= 0 (cst-%x0-9-nat abnf::cst)) (<= (cst-%x0-9-nat abnf::cst) 9))) :rule-classes :linear)
Theorem:
(defthm cst-%x0-29-nat-bounds (implies (cst-matchp abnf::cst "%x0-29") (and (<= 0 (cst-%x0-29-nat abnf::cst)) (<= (cst-%x0-29-nat abnf::cst) 41))) :rule-classes :linear)
Theorem:
(defthm cst-%xb-c-nat-bounds (implies (cst-matchp abnf::cst "%xB-C") (and (<= 11 (cst-%xb-c-nat abnf::cst)) (<= (cst-%xb-c-nat abnf::cst) 12))) :rule-classes :linear)
Theorem:
(defthm cst-%xe-7f-nat-bounds (implies (cst-matchp abnf::cst "%xE-7F") (and (<= 14 (cst-%xe-7f-nat abnf::cst)) (<= (cst-%xe-7f-nat abnf::cst) 127))) :rule-classes :linear)
Theorem:
(defthm cst-%x20-21-nat-bounds (implies (cst-matchp abnf::cst "%x20-21") (and (<= 32 (cst-%x20-21-nat abnf::cst)) (<= (cst-%x20-21-nat abnf::cst) 33))) :rule-classes :linear)
Theorem:
(defthm cst-%x20-26-nat-bounds (implies (cst-matchp abnf::cst "%x20-26") (and (<= 32 (cst-%x20-26-nat abnf::cst)) (<= (cst-%x20-26-nat abnf::cst) 38))) :rule-classes :linear)
Theorem:
(defthm cst-%x23-5b-nat-bounds (implies (cst-matchp abnf::cst "%x23-5B") (and (<= 35 (cst-%x23-5b-nat abnf::cst)) (<= (cst-%x23-5b-nat abnf::cst) 91))) :rule-classes :linear)
Theorem:
(defthm cst-%x28-5b-nat-bounds (implies (cst-matchp abnf::cst "%x28-5B") (and (<= 40 (cst-%x28-5b-nat abnf::cst)) (<= (cst-%x28-5b-nat abnf::cst) 91))) :rule-classes :linear)
Theorem:
(defthm cst-%x2b-2e-nat-bounds (implies (cst-matchp abnf::cst "%x2B-2E") (and (<= 43 (cst-%x2b-2e-nat abnf::cst)) (<= (cst-%x2b-2e-nat abnf::cst) 46))) :rule-classes :linear)
Theorem:
(defthm cst-%x2b-7f-nat-bounds (implies (cst-matchp abnf::cst "%x2B-7F") (and (<= 43 (cst-%x2b-7f-nat abnf::cst)) (<= (cst-%x2b-7f-nat abnf::cst) 127))) :rule-classes :linear)
Theorem:
(defthm cst-%x30-39-nat-bounds (implies (cst-matchp abnf::cst "%x30-39") (and (<= 48 (cst-%x30-39-nat abnf::cst)) (<= (cst-%x30-39-nat abnf::cst) 57))) :rule-classes :linear)
Theorem:
(defthm cst-%x30-7f-nat-bounds (implies (cst-matchp abnf::cst "%x30-7F") (and (<= 48 (cst-%x30-7f-nat abnf::cst)) (<= (cst-%x30-7f-nat abnf::cst) 127))) :rule-classes :linear)
Theorem:
(defthm cst-%x31-39-nat-bounds (implies (cst-matchp abnf::cst "%x31-39") (and (<= 49 (cst-%x31-39-nat abnf::cst)) (<= (cst-%x31-39-nat abnf::cst) 57))) :rule-classes :linear)
Theorem:
(defthm cst-%x41-5a-nat-bounds (implies (cst-matchp abnf::cst "%x41-5A") (and (<= 65 (cst-%x41-5a-nat abnf::cst)) (<= (cst-%x41-5a-nat abnf::cst) 90))) :rule-classes :linear)
Theorem:
(defthm cst-%x5d-7e-nat-bounds (implies (cst-matchp abnf::cst "%x5D-7E") (and (<= 93 (cst-%x5d-7e-nat abnf::cst)) (<= (cst-%x5d-7e-nat abnf::cst) 126))) :rule-classes :linear)
Theorem:
(defthm cst-%x61-7a-nat-bounds (implies (cst-matchp abnf::cst "%x61-7A") (and (<= 97 (cst-%x61-7a-nat abnf::cst)) (<= (cst-%x61-7a-nat abnf::cst) 122))) :rule-classes :linear)
Theorem:
(defthm |CST-"$"-LEAFTERM| (implies (cst-matchp abnf::cst "\"$\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"("-LEAFTERM| (implies (cst-matchp abnf::cst "\"(\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-")"-LEAFTERM| (implies (cst-matchp abnf::cst "\")\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"*"-LEAFTERM| (implies (cst-matchp abnf::cst "\"*\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-","-LEAFTERM| (implies (cst-matchp abnf::cst "\",\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"->"-LEAFTERM| (implies (cst-matchp abnf::cst "\"->\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"."-LEAFTERM| (implies (cst-matchp abnf::cst "\".\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"/"-LEAFTERM| (implies (cst-matchp abnf::cst "\"/\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"/*"-LEAFTERM| (implies (cst-matchp abnf::cst "\"/*\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"//"-LEAFTERM| (implies (cst-matchp abnf::cst "\"//\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"0"-LEAFTERM| (implies (cst-matchp abnf::cst "\"0\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-":="-LEAFTERM| (implies (cst-matchp abnf::cst "\":=\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"\\"-LEAFTERM| (implies (cst-matchp abnf::cst "\"\\\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"_"-LEAFTERM| (implies (cst-matchp abnf::cst "\"_\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"{"-LEAFTERM| (implies (cst-matchp abnf::cst "\"{\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-"}"-LEAFTERM| (implies (cst-matchp abnf::cst "\"}\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%i"a"-LEAFTERM| (implies (cst-matchp abnf::cst "%i\"a\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%i"b"-LEAFTERM| (implies (cst-matchp abnf::cst "%i\"b\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%i"c"-LEAFTERM| (implies (cst-matchp abnf::cst "%i\"c\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%i"d"-LEAFTERM| (implies (cst-matchp abnf::cst "%i\"d\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%i"e"-LEAFTERM| (implies (cst-matchp abnf::cst "%i\"e\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%i"f"-LEAFTERM| (implies (cst-matchp abnf::cst "%i\"f\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"0x"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"0x\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"\\"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"\\\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"break"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"break\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"case"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"case\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"continue"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"continue\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"default"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"default\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"false"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"false\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"for"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"for\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"function"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"function\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"hex"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"hex\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"if"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"if\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"leave"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"leave\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"let"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"let\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"n"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"n\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"r"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"r\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"switch"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"switch\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"t"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"t\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"true"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"true\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"u"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"u\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm |CST-%s"x"-LEAFTERM| (implies (cst-matchp abnf::cst "%s\"x\"") (equal (abnf::tree-kind abnf::cst) :leafterm)))
Theorem:
(defthm cst-boolean-nonleaf (implies (cst-matchp abnf::cst "boolean") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-dquote-nonleaf (implies (cst-matchp abnf::cst "dquote") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-squote-nonleaf (implies (cst-matchp abnf::cst "squote") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-lf-nonleaf (implies (cst-matchp abnf::cst "lf") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-cr-nonleaf (implies (cst-matchp abnf::cst "cr") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-decimal-digit-nonleaf (implies (cst-matchp abnf::cst "decimal-digit") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-nonzero-decimal-digit-nonleaf (implies (cst-matchp abnf::cst "nonzero-decimal-digit") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-hex-digit-nonleaf (implies (cst-matchp abnf::cst "hex-digit") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-decimal-number-nonleaf (implies (cst-matchp abnf::cst "decimal-number") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-hex-number-nonleaf (implies (cst-matchp abnf::cst "hex-number") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-hex-string-nonleaf (implies (cst-matchp abnf::cst "hex-string") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-double-quoted-printable-nonleaf (implies (cst-matchp abnf::cst "double-quoted-printable") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-single-quoted-printable-nonleaf (implies (cst-matchp abnf::cst "single-quoted-printable") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-escape-sequence-nonleaf (implies (cst-matchp abnf::cst "escape-sequence") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-string-literal-nonleaf (implies (cst-matchp abnf::cst "string-literal") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-literal-nonleaf (implies (cst-matchp abnf::cst "literal") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-lowercase-letter-nonleaf (implies (cst-matchp abnf::cst "lowercase-letter") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-uppercase-letter-nonleaf (implies (cst-matchp abnf::cst "uppercase-letter") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-identifier-start-nonleaf (implies (cst-matchp abnf::cst "identifier-start") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-identifier-rest-nonleaf (implies (cst-matchp abnf::cst "identifier-rest") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-identifier-nonleaf (implies (cst-matchp abnf::cst "identifier") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-keyword-nonleaf (implies (cst-matchp abnf::cst "keyword") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-symbol-nonleaf (implies (cst-matchp abnf::cst "symbol") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-whitespace-char-nonleaf (implies (cst-matchp abnf::cst "whitespace-char") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-whitespace-nonleaf (implies (cst-matchp abnf::cst "whitespace") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-not-star-nonleaf (implies (cst-matchp abnf::cst "not-star") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-not-star-or-slash-nonleaf (implies (cst-matchp abnf::cst "not-star-or-slash") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-block-comment-nonleaf (implies (cst-matchp abnf::cst "block-comment") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-rest-of-block-comment-nonleaf (implies (cst-matchp abnf::cst "rest-of-block-comment") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-rest-of-block-comment-after-star-nonleaf (implies (cst-matchp abnf::cst "rest-of-block-comment-after-star") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-not-lf-or-cr-nonleaf (implies (cst-matchp abnf::cst "not-lf-or-cr") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-end-of-line-comment-nonleaf (implies (cst-matchp abnf::cst "end-of-line-comment") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-comment-nonleaf (implies (cst-matchp abnf::cst "comment") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-token-nonleaf (implies (cst-matchp abnf::cst "token") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-lexeme-nonleaf (implies (cst-matchp abnf::cst "lexeme") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-path-nonleaf (implies (cst-matchp abnf::cst "path") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-expression-nonleaf (implies (cst-matchp abnf::cst "expression") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-function-call-nonleaf (implies (cst-matchp abnf::cst "function-call") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-function-definition-nonleaf (implies (cst-matchp abnf::cst "function-definition") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-if-statement-nonleaf (implies (cst-matchp abnf::cst "if-statement") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-for-statement-nonleaf (implies (cst-matchp abnf::cst "for-statement") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-switch-statement-nonleaf (implies (cst-matchp abnf::cst "switch-statement") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-assignment-nonleaf (implies (cst-matchp abnf::cst "assignment") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-variable-declaration-nonleaf (implies (cst-matchp abnf::cst "variable-declaration") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-block-nonleaf (implies (cst-matchp abnf::cst "block") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-statement-nonleaf (implies (cst-matchp abnf::cst "statement") (equal (abnf::tree-kind abnf::cst) :nonleaf)))
Theorem:
(defthm cst-boolean-rulename (implies (cst-matchp abnf::cst "boolean") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "boolean"))))
Theorem:
(defthm cst-dquote-rulename (implies (cst-matchp abnf::cst "dquote") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "dquote"))))
Theorem:
(defthm cst-squote-rulename (implies (cst-matchp abnf::cst "squote") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "squote"))))
Theorem:
(defthm cst-lf-rulename (implies (cst-matchp abnf::cst "lf") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "lf"))))
Theorem:
(defthm cst-cr-rulename (implies (cst-matchp abnf::cst "cr") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "cr"))))
Theorem:
(defthm cst-decimal-digit-rulename (implies (cst-matchp abnf::cst "decimal-digit") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "decimal-digit"))))
Theorem:
(defthm cst-nonzero-decimal-digit-rulename (implies (cst-matchp abnf::cst "nonzero-decimal-digit") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "nonzero-decimal-digit"))))
Theorem:
(defthm cst-hex-digit-rulename (implies (cst-matchp abnf::cst "hex-digit") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "hex-digit"))))
Theorem:
(defthm cst-decimal-number-rulename (implies (cst-matchp abnf::cst "decimal-number") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "decimal-number"))))
Theorem:
(defthm cst-hex-number-rulename (implies (cst-matchp abnf::cst "hex-number") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "hex-number"))))
Theorem:
(defthm cst-hex-string-rulename (implies (cst-matchp abnf::cst "hex-string") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "hex-string"))))
Theorem:
(defthm cst-double-quoted-printable-rulename (implies (cst-matchp abnf::cst "double-quoted-printable") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "double-quoted-printable"))))
Theorem:
(defthm cst-single-quoted-printable-rulename (implies (cst-matchp abnf::cst "single-quoted-printable") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "single-quoted-printable"))))
Theorem:
(defthm cst-escape-sequence-rulename (implies (cst-matchp abnf::cst "escape-sequence") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "escape-sequence"))))
Theorem:
(defthm cst-string-literal-rulename (implies (cst-matchp abnf::cst "string-literal") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "string-literal"))))
Theorem:
(defthm cst-literal-rulename (implies (cst-matchp abnf::cst "literal") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "literal"))))
Theorem:
(defthm cst-lowercase-letter-rulename (implies (cst-matchp abnf::cst "lowercase-letter") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "lowercase-letter"))))
Theorem:
(defthm cst-uppercase-letter-rulename (implies (cst-matchp abnf::cst "uppercase-letter") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "uppercase-letter"))))
Theorem:
(defthm cst-identifier-start-rulename (implies (cst-matchp abnf::cst "identifier-start") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "identifier-start"))))
Theorem:
(defthm cst-identifier-rest-rulename (implies (cst-matchp abnf::cst "identifier-rest") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "identifier-rest"))))
Theorem:
(defthm cst-identifier-rulename (implies (cst-matchp abnf::cst "identifier") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "identifier"))))
Theorem:
(defthm cst-keyword-rulename (implies (cst-matchp abnf::cst "keyword") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "keyword"))))
Theorem:
(defthm cst-symbol-rulename (implies (cst-matchp abnf::cst "symbol") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "symbol"))))
Theorem:
(defthm cst-whitespace-char-rulename (implies (cst-matchp abnf::cst "whitespace-char") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "whitespace-char"))))
Theorem:
(defthm cst-whitespace-rulename (implies (cst-matchp abnf::cst "whitespace") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "whitespace"))))
Theorem:
(defthm cst-not-star-rulename (implies (cst-matchp abnf::cst "not-star") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "not-star"))))
Theorem:
(defthm cst-not-star-or-slash-rulename (implies (cst-matchp abnf::cst "not-star-or-slash") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "not-star-or-slash"))))
Theorem:
(defthm cst-block-comment-rulename (implies (cst-matchp abnf::cst "block-comment") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "block-comment"))))
Theorem:
(defthm cst-rest-of-block-comment-rulename (implies (cst-matchp abnf::cst "rest-of-block-comment") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "rest-of-block-comment"))))
Theorem:
(defthm cst-rest-of-block-comment-after-star-rulename (implies (cst-matchp abnf::cst "rest-of-block-comment-after-star") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "rest-of-block-comment-after-star"))))
Theorem:
(defthm cst-not-lf-or-cr-rulename (implies (cst-matchp abnf::cst "not-lf-or-cr") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "not-lf-or-cr"))))
Theorem:
(defthm cst-end-of-line-comment-rulename (implies (cst-matchp abnf::cst "end-of-line-comment") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "end-of-line-comment"))))
Theorem:
(defthm cst-comment-rulename (implies (cst-matchp abnf::cst "comment") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "comment"))))
Theorem:
(defthm cst-token-rulename (implies (cst-matchp abnf::cst "token") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "token"))))
Theorem:
(defthm cst-lexeme-rulename (implies (cst-matchp abnf::cst "lexeme") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "lexeme"))))
Theorem:
(defthm cst-path-rulename (implies (cst-matchp abnf::cst "path") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "path"))))
Theorem:
(defthm cst-expression-rulename (implies (cst-matchp abnf::cst "expression") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "expression"))))
Theorem:
(defthm cst-function-call-rulename (implies (cst-matchp abnf::cst "function-call") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "function-call"))))
Theorem:
(defthm cst-function-definition-rulename (implies (cst-matchp abnf::cst "function-definition") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "function-definition"))))
Theorem:
(defthm cst-if-statement-rulename (implies (cst-matchp abnf::cst "if-statement") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "if-statement"))))
Theorem:
(defthm cst-for-statement-rulename (implies (cst-matchp abnf::cst "for-statement") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "for-statement"))))
Theorem:
(defthm cst-switch-statement-rulename (implies (cst-matchp abnf::cst "switch-statement") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "switch-statement"))))
Theorem:
(defthm cst-assignment-rulename (implies (cst-matchp abnf::cst "assignment") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "assignment"))))
Theorem:
(defthm cst-variable-declaration-rulename (implies (cst-matchp abnf::cst "variable-declaration") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "variable-declaration"))))
Theorem:
(defthm cst-block-rulename (implies (cst-matchp abnf::cst "block") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "block"))))
Theorem:
(defthm cst-statement-rulename (implies (cst-matchp abnf::cst "statement") (equal (abnf::tree-nonleaf->rulename? abnf::cst) (abnf::rulename "statement"))))
Theorem:
(defthm cst-boolean-branches-match-alt (implies (cst-matchp abnf::cst "boolean") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"true\" / %s\"false\"")))
Theorem:
(defthm cst-dquote-branches-match-alt (implies (cst-matchp abnf::cst "dquote") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x22")))
Theorem:
(defthm cst-squote-branches-match-alt (implies (cst-matchp abnf::cst "squote") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x27")))
Theorem:
(defthm cst-lf-branches-match-alt (implies (cst-matchp abnf::cst "lf") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%xA")))
Theorem:
(defthm cst-cr-branches-match-alt (implies (cst-matchp abnf::cst "cr") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%xD")))
Theorem:
(defthm cst-decimal-digit-branches-match-alt (implies (cst-matchp abnf::cst "decimal-digit") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x30-39")))
Theorem:
(defthm cst-nonzero-decimal-digit-branches-match-alt (implies (cst-matchp abnf::cst "nonzero-decimal-digit") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x31-39")))
Theorem:
(defthm cst-hex-digit-branches-match-alt (implies (cst-matchp abnf::cst "hex-digit") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "decimal-digit / %i\"a\" / %i\"b\" / %i\"c\" / %i\"d\" / %i\"e\" / %i\"f\"")))
Theorem:
(defthm cst-decimal-number-branches-match-alt (implies (cst-matchp abnf::cst "decimal-number") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"0\" / nonzero-decimal-digit *decimal-digit")))
Theorem:
(defthm cst-hex-number-branches-match-alt (implies (cst-matchp abnf::cst "hex-number") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"0x\" *hex-digit")))
Theorem:
(defthm cst-hex-string-branches-match-alt (implies (cst-matchp abnf::cst "hex-string") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"hex\" ( dquote [ 2hex-digit *( [ \"_\" ] 2hex-digit ) ] dquote / squote [ 2hex-digit *( [ \"_\" ] 2hex-digit ) ] squote )")))
Theorem:
(defthm cst-double-quoted-printable-branches-match-alt (implies (cst-matchp abnf::cst "double-quoted-printable") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x20-21 / %x23-5B / %x5D-7E")))
Theorem:
(defthm cst-single-quoted-printable-branches-match-alt (implies (cst-matchp abnf::cst "single-quoted-printable") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x20-26 / %x28-5B / %x5D-7E")))
Theorem:
(defthm cst-escape-sequence-branches-match-alt (implies (cst-matchp abnf::cst "escape-sequence") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"\\\" ( ( squote / dquote / %s\"\\\" / %s\"n\" / %s\"r\" / %s\"t\" / lf / cr ) / %s\"u\" 4hex-digit / %s\"x\" 2hex-digit )")))
Theorem:
(defthm cst-string-literal-branches-match-alt (implies (cst-matchp abnf::cst "string-literal") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "dquote *( double-quoted-printable / escape-sequence ) dquote / squote *( single-quoted-printable / escape-sequence ) squote")))
Theorem:
(defthm cst-literal-branches-match-alt (implies (cst-matchp abnf::cst "literal") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "decimal-number / hex-number / boolean / string-literal / hex-string")))
Theorem:
(defthm cst-lowercase-letter-branches-match-alt (implies (cst-matchp abnf::cst "lowercase-letter") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x61-7A")))
Theorem:
(defthm cst-uppercase-letter-branches-match-alt (implies (cst-matchp abnf::cst "uppercase-letter") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x41-5A")))
Theorem:
(defthm cst-identifier-start-branches-match-alt (implies (cst-matchp abnf::cst "identifier-start") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "lowercase-letter / uppercase-letter / \"$\" / \"_\"")))
Theorem:
(defthm cst-identifier-rest-branches-match-alt (implies (cst-matchp abnf::cst "identifier-rest") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier-start / decimal-digit")))
Theorem:
(defthm cst-identifier-branches-match-alt (implies (cst-matchp abnf::cst "identifier") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier-start *identifier-rest")))
Theorem:
(defthm cst-keyword-branches-match-alt (implies (cst-matchp abnf::cst "keyword") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"function\" / %s\"if\" / %s\"for\" / %s\"switch\" / %s\"case\" / %s\"default\" / %s\"let\" / %s\"leave\" / %s\"break\" / %s\"continue\"")))
Theorem:
(defthm cst-symbol-branches-match-alt (implies (cst-matchp abnf::cst "symbol") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\".\" / \",\" / \"->\" / \"(\" / \")\" / \":=\" / \"{\" / \"}\"")))
Theorem:
(defthm cst-whitespace-char-branches-match-alt (implies (cst-matchp abnf::cst "whitespace-char") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x20 / %x9 / %xD / %xA / %xC")))
Theorem:
(defthm cst-whitespace-branches-match-alt (implies (cst-matchp abnf::cst "whitespace") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "1*whitespace-char")))
Theorem:
(defthm cst-not-star-branches-match-alt (implies (cst-matchp abnf::cst "not-star") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x0-29 / %x2B-7F")))
Theorem:
(defthm cst-not-star-or-slash-branches-match-alt (implies (cst-matchp abnf::cst "not-star-or-slash") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x0-29 / %x2B-2E / %x30-7F")))
Theorem:
(defthm cst-block-comment-branches-match-alt (implies (cst-matchp abnf::cst "block-comment") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"/*\" rest-of-block-comment")))
Theorem:
(defthm cst-rest-of-block-comment-branches-match-alt (implies (cst-matchp abnf::cst "rest-of-block-comment") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"*\" rest-of-block-comment-after-star / not-star rest-of-block-comment")))
Theorem:
(defthm cst-rest-of-block-comment-after-star-branches-match-alt (implies (cst-matchp abnf::cst "rest-of-block-comment-after-star") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"/\" / \"*\" rest-of-block-comment-after-star / not-star-or-slash rest-of-block-comment")))
Theorem:
(defthm cst-not-lf-or-cr-branches-match-alt (implies (cst-matchp abnf::cst "not-lf-or-cr") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%x0-9 / %xB-C / %xE-7F")))
Theorem:
(defthm cst-end-of-line-comment-branches-match-alt (implies (cst-matchp abnf::cst "end-of-line-comment") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"//\" *not-lf-or-cr")))
Theorem:
(defthm cst-comment-branches-match-alt (implies (cst-matchp abnf::cst "comment") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "block-comment / end-of-line-comment")))
Theorem:
(defthm cst-token-branches-match-alt (implies (cst-matchp abnf::cst "token") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "keyword / literal / identifier / symbol")))
Theorem:
(defthm cst-lexeme-branches-match-alt (implies (cst-matchp abnf::cst "lexeme") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "token / comment / whitespace")))
Theorem:
(defthm cst-path-branches-match-alt (implies (cst-matchp abnf::cst "path") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier *( \".\" identifier )")))
Theorem:
(defthm cst-expression-branches-match-alt (implies (cst-matchp abnf::cst "expression") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "path / function-call / literal")))
Theorem:
(defthm cst-function-call-branches-match-alt (implies (cst-matchp abnf::cst "function-call") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier \"(\" [ expression *( \",\" expression ) ] \")\"")))
Theorem:
(defthm cst-function-definition-branches-match-alt (implies (cst-matchp abnf::cst "function-definition") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"function\" identifier \"(\" [ identifier *( \",\" identifier ) ] \")\" [ \"->\" identifier *( \",\" identifier ) ] block")))
Theorem:
(defthm cst-if-statement-branches-match-alt (implies (cst-matchp abnf::cst "if-statement") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"if\" expression block")))
Theorem:
(defthm cst-for-statement-branches-match-alt (implies (cst-matchp abnf::cst "for-statement") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"for\" block expression block block")))
Theorem:
(defthm cst-switch-statement-branches-match-alt (implies (cst-matchp abnf::cst "switch-statement") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"switch\" expression ( 1*( %s\"case\" literal block ) [ %s\"default\" block ] / %s\"default\" block )")))
Theorem:
(defthm cst-assignment-branches-match-alt (implies (cst-matchp abnf::cst "assignment") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "path \":=\" expression / path 1*( \",\" path ) \":=\" function-call")))
Theorem:
(defthm cst-variable-declaration-branches-match-alt (implies (cst-matchp abnf::cst "variable-declaration") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "%s\"let\" identifier [ \":=\" expression ] / %s\"let\" identifier *( \",\" identifier ) [ \":=\" function-call ]")))
Theorem:
(defthm cst-block-branches-match-alt (implies (cst-matchp abnf::cst "block") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "\"{\" *statement \"}\"")))
Theorem:
(defthm cst-statement-branches-match-alt (implies (cst-matchp abnf::cst "statement") (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst) "block / variable-declaration / assignment / function-call / if-statement / for-statement / switch-statement / %s\"leave\" / %s\"break\" / %s\"continue\" / function-definition")))
Theorem:
(defthm cst-boolean-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"true\" / %s\"false\"") (or (cst-list-list-conc-matchp abnf::cstss "%s\"true\"") (cst-list-list-conc-matchp abnf::cstss "%s\"false\""))))
Theorem:
(defthm cst-dquote-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x22") (or (cst-list-list-conc-matchp abnf::cstss "%x22"))))
Theorem:
(defthm cst-squote-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x27") (or (cst-list-list-conc-matchp abnf::cstss "%x27"))))
Theorem:
(defthm cst-lf-concs (implies (cst-list-list-alt-matchp abnf::cstss "%xA") (or (cst-list-list-conc-matchp abnf::cstss "%xA"))))
Theorem:
(defthm cst-cr-concs (implies (cst-list-list-alt-matchp abnf::cstss "%xD") (or (cst-list-list-conc-matchp abnf::cstss "%xD"))))
Theorem:
(defthm cst-decimal-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-nonzero-decimal-digit-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x31-39") (or (cst-list-list-conc-matchp abnf::cstss "%x31-39"))))
Theorem:
(defthm cst-hex-digit-concs (implies (cst-list-list-alt-matchp abnf::cstss "decimal-digit / %i\"a\" / %i\"b\" / %i\"c\" / %i\"d\" / %i\"e\" / %i\"f\"") (or (cst-list-list-conc-matchp abnf::cstss "decimal-digit") (cst-list-list-conc-matchp abnf::cstss "%i\"a\"") (cst-list-list-conc-matchp abnf::cstss "%i\"b\"") (cst-list-list-conc-matchp abnf::cstss "%i\"c\"") (cst-list-list-conc-matchp abnf::cstss "%i\"d\"") (cst-list-list-conc-matchp abnf::cstss "%i\"e\"") (cst-list-list-conc-matchp abnf::cstss "%i\"f\""))))
Theorem:
(defthm cst-decimal-number-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"0\" / nonzero-decimal-digit *decimal-digit") (or (cst-list-list-conc-matchp abnf::cstss "\"0\"") (cst-list-list-conc-matchp abnf::cstss "nonzero-decimal-digit *decimal-digit"))))
Theorem:
(defthm cst-hex-number-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"0x\" *hex-digit") (or (cst-list-list-conc-matchp abnf::cstss "%s\"0x\" *hex-digit"))))
Theorem:
(defthm cst-hex-string-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"hex\" ( dquote [ 2hex-digit *( [ \"_\" ] 2hex-digit ) ] dquote / squote [ 2hex-digit *( [ \"_\" ] 2hex-digit ) ] squote )") (or (cst-list-list-conc-matchp abnf::cstss "%s\"hex\" ( dquote [ 2hex-digit *( [ \"_\" ] 2hex-digit ) ] dquote / squote [ 2hex-digit *( [ \"_\" ] 2hex-digit ) ] squote )"))))
Theorem:
(defthm cst-double-quoted-printable-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x20-21 / %x23-5B / %x5D-7E") (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-7E"))))
Theorem:
(defthm cst-single-quoted-printable-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x20-26 / %x28-5B / %x5D-7E") (or (cst-list-list-conc-matchp abnf::cstss "%x20-26") (cst-list-list-conc-matchp abnf::cstss "%x28-5B") (cst-list-list-conc-matchp abnf::cstss "%x5D-7E"))))
Theorem:
(defthm cst-escape-sequence-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"\\\" ( ( squote / dquote / %s\"\\\" / %s\"n\" / %s\"r\" / %s\"t\" / lf / cr ) / %s\"u\" 4hex-digit / %s\"x\" 2hex-digit )") (or (cst-list-list-conc-matchp abnf::cstss "\"\\\" ( ( squote / dquote / %s\"\\\" / %s\"n\" / %s\"r\" / %s\"t\" / lf / cr ) / %s\"u\" 4hex-digit / %s\"x\" 2hex-digit )"))))
Theorem:
(defthm cst-string-literal-concs (implies (cst-list-list-alt-matchp abnf::cstss "dquote *( double-quoted-printable / escape-sequence ) dquote / squote *( single-quoted-printable / escape-sequence ) squote") (or (cst-list-list-conc-matchp abnf::cstss "dquote *( double-quoted-printable / escape-sequence ) dquote") (cst-list-list-conc-matchp abnf::cstss "squote *( single-quoted-printable / escape-sequence ) squote"))))
Theorem:
(defthm cst-literal-concs (implies (cst-list-list-alt-matchp abnf::cstss "decimal-number / hex-number / boolean / string-literal / hex-string") (or (cst-list-list-conc-matchp abnf::cstss "decimal-number") (cst-list-list-conc-matchp abnf::cstss "hex-number") (cst-list-list-conc-matchp abnf::cstss "boolean") (cst-list-list-conc-matchp abnf::cstss "string-literal") (cst-list-list-conc-matchp abnf::cstss "hex-string"))))
Theorem:
(defthm cst-lowercase-letter-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x61-7A") (or (cst-list-list-conc-matchp abnf::cstss "%x61-7A"))))
Theorem:
(defthm cst-uppercase-letter-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x41-5A") (or (cst-list-list-conc-matchp abnf::cstss "%x41-5A"))))
Theorem:
(defthm cst-identifier-start-concs (implies (cst-list-list-alt-matchp abnf::cstss "lowercase-letter / uppercase-letter / \"$\" / \"_\"") (or (cst-list-list-conc-matchp abnf::cstss "lowercase-letter") (cst-list-list-conc-matchp abnf::cstss "uppercase-letter") (cst-list-list-conc-matchp abnf::cstss "\"$\"") (cst-list-list-conc-matchp abnf::cstss "\"_\""))))
Theorem:
(defthm cst-identifier-rest-concs (implies (cst-list-list-alt-matchp abnf::cstss "identifier-start / decimal-digit") (or (cst-list-list-conc-matchp abnf::cstss "identifier-start") (cst-list-list-conc-matchp abnf::cstss "decimal-digit"))))
Theorem:
(defthm cst-identifier-concs (implies (cst-list-list-alt-matchp abnf::cstss "identifier-start *identifier-rest") (or (cst-list-list-conc-matchp abnf::cstss "identifier-start *identifier-rest"))))
Theorem:
(defthm cst-keyword-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"function\" / %s\"if\" / %s\"for\" / %s\"switch\" / %s\"case\" / %s\"default\" / %s\"let\" / %s\"leave\" / %s\"break\" / %s\"continue\"") (or (cst-list-list-conc-matchp abnf::cstss "%s\"function\"") (cst-list-list-conc-matchp abnf::cstss "%s\"if\"") (cst-list-list-conc-matchp abnf::cstss "%s\"for\"") (cst-list-list-conc-matchp abnf::cstss "%s\"switch\"") (cst-list-list-conc-matchp abnf::cstss "%s\"case\"") (cst-list-list-conc-matchp abnf::cstss "%s\"default\"") (cst-list-list-conc-matchp abnf::cstss "%s\"let\"") (cst-list-list-conc-matchp abnf::cstss "%s\"leave\"") (cst-list-list-conc-matchp abnf::cstss "%s\"break\"") (cst-list-list-conc-matchp abnf::cstss "%s\"continue\""))))
Theorem:
(defthm cst-symbol-concs (implies (cst-list-list-alt-matchp abnf::cstss "\".\" / \",\" / \"->\" / \"(\" / \")\" / \":=\" / \"{\" / \"}\"") (or (cst-list-list-conc-matchp abnf::cstss "\".\"") (cst-list-list-conc-matchp abnf::cstss "\",\"") (cst-list-list-conc-matchp abnf::cstss "\"->\"") (cst-list-list-conc-matchp abnf::cstss "\"(\"") (cst-list-list-conc-matchp abnf::cstss "\")\"") (cst-list-list-conc-matchp abnf::cstss "\":=\"") (cst-list-list-conc-matchp abnf::cstss "\"{\"") (cst-list-list-conc-matchp abnf::cstss "\"}\""))))
Theorem:
(defthm cst-whitespace-char-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x20 / %x9 / %xD / %xA / %xC") (or (cst-list-list-conc-matchp abnf::cstss "%x20") (cst-list-list-conc-matchp abnf::cstss "%x9") (cst-list-list-conc-matchp abnf::cstss "%xD") (cst-list-list-conc-matchp abnf::cstss "%xA") (cst-list-list-conc-matchp abnf::cstss "%xC"))))
Theorem:
(defthm cst-whitespace-concs (implies (cst-list-list-alt-matchp abnf::cstss "1*whitespace-char") (or (cst-list-list-conc-matchp abnf::cstss "1*whitespace-char"))))
Theorem:
(defthm cst-not-star-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x0-29 / %x2B-7F") (or (cst-list-list-conc-matchp abnf::cstss "%x0-29") (cst-list-list-conc-matchp abnf::cstss "%x2B-7F"))))
Theorem:
(defthm cst-not-star-or-slash-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x0-29 / %x2B-2E / %x30-7F") (or (cst-list-list-conc-matchp abnf::cstss "%x0-29") (cst-list-list-conc-matchp abnf::cstss "%x2B-2E") (cst-list-list-conc-matchp abnf::cstss "%x30-7F"))))
Theorem:
(defthm cst-block-comment-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"/*\" rest-of-block-comment") (or (cst-list-list-conc-matchp abnf::cstss "\"/*\" rest-of-block-comment"))))
Theorem:
(defthm cst-rest-of-block-comment-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"*\" rest-of-block-comment-after-star / not-star rest-of-block-comment") (or (cst-list-list-conc-matchp abnf::cstss "\"*\" rest-of-block-comment-after-star") (cst-list-list-conc-matchp abnf::cstss "not-star rest-of-block-comment"))))
Theorem:
(defthm cst-rest-of-block-comment-after-star-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"/\" / \"*\" rest-of-block-comment-after-star / not-star-or-slash rest-of-block-comment") (or (cst-list-list-conc-matchp abnf::cstss "\"/\"") (cst-list-list-conc-matchp abnf::cstss "\"*\" rest-of-block-comment-after-star") (cst-list-list-conc-matchp abnf::cstss "not-star-or-slash rest-of-block-comment"))))
Theorem:
(defthm cst-not-lf-or-cr-concs (implies (cst-list-list-alt-matchp abnf::cstss "%x0-9 / %xB-C / %xE-7F") (or (cst-list-list-conc-matchp abnf::cstss "%x0-9") (cst-list-list-conc-matchp abnf::cstss "%xB-C") (cst-list-list-conc-matchp abnf::cstss "%xE-7F"))))
Theorem:
(defthm cst-end-of-line-comment-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"//\" *not-lf-or-cr") (or (cst-list-list-conc-matchp abnf::cstss "\"//\" *not-lf-or-cr"))))
Theorem:
(defthm cst-comment-concs (implies (cst-list-list-alt-matchp abnf::cstss "block-comment / end-of-line-comment") (or (cst-list-list-conc-matchp abnf::cstss "block-comment") (cst-list-list-conc-matchp abnf::cstss "end-of-line-comment"))))
Theorem:
(defthm cst-token-concs (implies (cst-list-list-alt-matchp abnf::cstss "keyword / literal / identifier / symbol") (or (cst-list-list-conc-matchp abnf::cstss "keyword") (cst-list-list-conc-matchp abnf::cstss "literal") (cst-list-list-conc-matchp abnf::cstss "identifier") (cst-list-list-conc-matchp abnf::cstss "symbol"))))
Theorem:
(defthm cst-lexeme-concs (implies (cst-list-list-alt-matchp abnf::cstss "token / comment / whitespace") (or (cst-list-list-conc-matchp abnf::cstss "token") (cst-list-list-conc-matchp abnf::cstss "comment") (cst-list-list-conc-matchp abnf::cstss "whitespace"))))
Theorem:
(defthm cst-path-concs (implies (cst-list-list-alt-matchp abnf::cstss "identifier *( \".\" identifier )") (or (cst-list-list-conc-matchp abnf::cstss "identifier *( \".\" identifier )"))))
Theorem:
(defthm cst-expression-concs (implies (cst-list-list-alt-matchp abnf::cstss "path / function-call / literal") (or (cst-list-list-conc-matchp abnf::cstss "path") (cst-list-list-conc-matchp abnf::cstss "function-call") (cst-list-list-conc-matchp abnf::cstss "literal"))))
Theorem:
(defthm cst-function-call-concs (implies (cst-list-list-alt-matchp abnf::cstss "identifier \"(\" [ expression *( \",\" expression ) ] \")\"") (or (cst-list-list-conc-matchp abnf::cstss "identifier \"(\" [ expression *( \",\" expression ) ] \")\""))))
Theorem:
(defthm cst-function-definition-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"function\" identifier \"(\" [ identifier *( \",\" identifier ) ] \")\" [ \"->\" identifier *( \",\" identifier ) ] block") (or (cst-list-list-conc-matchp abnf::cstss "%s\"function\" identifier \"(\" [ identifier *( \",\" identifier ) ] \")\" [ \"->\" identifier *( \",\" identifier ) ] block"))))
Theorem:
(defthm cst-if-statement-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"if\" expression block") (or (cst-list-list-conc-matchp abnf::cstss "%s\"if\" expression block"))))
Theorem:
(defthm cst-for-statement-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"for\" block expression block block") (or (cst-list-list-conc-matchp abnf::cstss "%s\"for\" block expression block block"))))
Theorem:
(defthm cst-switch-statement-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"switch\" expression ( 1*( %s\"case\" literal block ) [ %s\"default\" block ] / %s\"default\" block )") (or (cst-list-list-conc-matchp abnf::cstss "%s\"switch\" expression ( 1*( %s\"case\" literal block ) [ %s\"default\" block ] / %s\"default\" block )"))))
Theorem:
(defthm cst-assignment-concs (implies (cst-list-list-alt-matchp abnf::cstss "path \":=\" expression / path 1*( \",\" path ) \":=\" function-call") (or (cst-list-list-conc-matchp abnf::cstss "path \":=\" expression") (cst-list-list-conc-matchp abnf::cstss "path 1*( \",\" path ) \":=\" function-call"))))
Theorem:
(defthm cst-variable-declaration-concs (implies (cst-list-list-alt-matchp abnf::cstss "%s\"let\" identifier [ \":=\" expression ] / %s\"let\" identifier *( \",\" identifier ) [ \":=\" function-call ]") (or (cst-list-list-conc-matchp abnf::cstss "%s\"let\" identifier [ \":=\" expression ]") (cst-list-list-conc-matchp abnf::cstss "%s\"let\" identifier *( \",\" identifier ) [ \":=\" function-call ]"))))
Theorem:
(defthm cst-block-concs (implies (cst-list-list-alt-matchp abnf::cstss "\"{\" *statement \"}\"") (or (cst-list-list-conc-matchp abnf::cstss "\"{\" *statement \"}\""))))
Theorem:
(defthm cst-statement-concs (implies (cst-list-list-alt-matchp abnf::cstss "block / variable-declaration / assignment / function-call / if-statement / for-statement / switch-statement / %s\"leave\" / %s\"break\" / %s\"continue\" / function-definition") (or (cst-list-list-conc-matchp abnf::cstss "block") (cst-list-list-conc-matchp abnf::cstss "variable-declaration") (cst-list-list-conc-matchp abnf::cstss "assignment") (cst-list-list-conc-matchp abnf::cstss "function-call") (cst-list-list-conc-matchp abnf::cstss "if-statement") (cst-list-list-conc-matchp abnf::cstss "for-statement") (cst-list-list-conc-matchp abnf::cstss "switch-statement") (cst-list-list-conc-matchp abnf::cstss "%s\"leave\"") (cst-list-list-conc-matchp abnf::cstss "%s\"break\"") (cst-list-list-conc-matchp abnf::cstss "%s\"continue\"") (cst-list-list-conc-matchp abnf::cstss "function-definition"))))
Theorem:
(defthm cst-boolean-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"true\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"true\""))))
Theorem:
(defthm cst-boolean-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"false\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"false\""))))
Theorem:
(defthm cst-dquote-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-squote-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x27") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x27"))))
Theorem:
(defthm cst-lf-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xA") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xA"))))
Theorem:
(defthm cst-cr-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xD") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xD"))))
Theorem:
(defthm cst-decimal-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-nonzero-decimal-digit-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-hex-digit-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "decimal-digit") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "decimal-digit"))))
Theorem:
(defthm cst-hex-digit-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%i\"a\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%i\"a\""))))
Theorem:
(defthm cst-hex-digit-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "%i\"b\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%i\"b\""))))
Theorem:
(defthm cst-hex-digit-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "%i\"c\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%i\"c\""))))
Theorem:
(defthm cst-hex-digit-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "%i\"d\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%i\"d\""))))
Theorem:
(defthm cst-hex-digit-conc6-matching (implies (cst-list-list-conc-matchp abnf::cstss "%i\"e\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%i\"e\""))))
Theorem:
(defthm cst-hex-digit-conc7-matching (implies (cst-list-list-conc-matchp abnf::cstss "%i\"f\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%i\"f\""))))
Theorem:
(defthm cst-decimal-number-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"0\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"0\""))))
Theorem:
(defthm cst-double-quoted-printable-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-double-quoted-printable-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-double-quoted-printable-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x5D-7E") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x5D-7E"))))
Theorem:
(defthm cst-single-quoted-printable-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x20-26") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x20-26"))))
Theorem:
(defthm cst-single-quoted-printable-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x28-5B") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x28-5B"))))
Theorem:
(defthm cst-single-quoted-printable-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x5D-7E") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x5D-7E"))))
Theorem:
(defthm cst-literal-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "decimal-number") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "decimal-number"))))
Theorem:
(defthm cst-literal-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "hex-number") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "hex-number"))))
Theorem:
(defthm cst-literal-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "boolean") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "boolean"))))
Theorem:
(defthm cst-literal-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "string-literal") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "string-literal"))))
Theorem:
(defthm cst-literal-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "hex-string") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "hex-string"))))
Theorem:
(defthm cst-lowercase-letter-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x61-7A") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x61-7A"))))
Theorem:
(defthm cst-uppercase-letter-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x41-5A") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x41-5A"))))
Theorem:
(defthm cst-identifier-start-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "lowercase-letter") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "lowercase-letter"))))
Theorem:
(defthm cst-identifier-start-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "uppercase-letter") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "uppercase-letter"))))
Theorem:
(defthm cst-identifier-start-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"$\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"$\""))))
Theorem:
(defthm cst-identifier-start-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"_\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"_\""))))
Theorem:
(defthm cst-identifier-rest-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "identifier-start") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "identifier-start"))))
Theorem:
(defthm cst-identifier-rest-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "decimal-digit") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "decimal-digit"))))
Theorem:
(defthm cst-keyword-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"function\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"function\""))))
Theorem:
(defthm cst-keyword-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"if\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"if\""))))
Theorem:
(defthm cst-keyword-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"for\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"for\""))))
Theorem:
(defthm cst-keyword-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"switch\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"switch\""))))
Theorem:
(defthm cst-keyword-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"case\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"case\""))))
Theorem:
(defthm cst-keyword-conc6-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"default\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"default\""))))
Theorem:
(defthm cst-keyword-conc7-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"let\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"let\""))))
Theorem:
(defthm cst-keyword-conc8-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"leave\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"leave\""))))
Theorem:
(defthm cst-keyword-conc9-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"break\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"break\""))))
Theorem:
(defthm cst-keyword-conc10-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"continue\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"continue\""))))
Theorem:
(defthm cst-symbol-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "\".\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\".\""))))
Theorem:
(defthm cst-symbol-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "\",\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\",\""))))
Theorem:
(defthm cst-symbol-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"->\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"->\""))))
Theorem:
(defthm cst-symbol-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"(\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"(\""))))
Theorem:
(defthm cst-symbol-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "\")\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\")\""))))
Theorem:
(defthm cst-symbol-conc6-matching (implies (cst-list-list-conc-matchp abnf::cstss "\":=\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\":=\""))))
Theorem:
(defthm cst-symbol-conc7-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"{\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"{\""))))
Theorem:
(defthm cst-symbol-conc8-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"}\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"}\""))))
Theorem:
(defthm cst-whitespace-char-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x20") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x20"))))
Theorem:
(defthm cst-whitespace-char-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x9") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x9"))))
Theorem:
(defthm cst-whitespace-char-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xD") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xD"))))
Theorem:
(defthm cst-whitespace-char-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xA") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xA"))))
Theorem:
(defthm cst-whitespace-char-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xC") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xC"))))
Theorem:
(defthm cst-whitespace-conc-matching (implies (cst-list-list-conc-matchp abnf::cstss "1*whitespace-char") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "1*whitespace-char"))))
Theorem:
(defthm cst-not-star-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x0-29") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x0-29"))))
Theorem:
(defthm cst-not-star-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x2B-7F") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x2B-7F"))))
Theorem:
(defthm cst-not-star-or-slash-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x0-29") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x0-29"))))
Theorem:
(defthm cst-not-star-or-slash-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x2B-2E") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x2B-2E"))))
Theorem:
(defthm cst-not-star-or-slash-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x30-7F") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x30-7F"))))
Theorem:
(defthm cst-rest-of-block-comment-after-star-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "\"/\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "\"/\""))))
Theorem:
(defthm cst-not-lf-or-cr-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "%x0-9") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%x0-9"))))
Theorem:
(defthm cst-not-lf-or-cr-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xB-C") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xB-C"))))
Theorem:
(defthm cst-not-lf-or-cr-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "%xE-7F") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%xE-7F"))))
Theorem:
(defthm cst-comment-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "block-comment") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "block-comment"))))
Theorem:
(defthm cst-comment-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "end-of-line-comment") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "end-of-line-comment"))))
Theorem:
(defthm cst-token-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "keyword") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "keyword"))))
Theorem:
(defthm cst-token-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "literal") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "literal"))))
Theorem:
(defthm cst-token-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "identifier") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "identifier"))))
Theorem:
(defthm cst-token-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "symbol") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "symbol"))))
Theorem:
(defthm cst-lexeme-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "token") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "token"))))
Theorem:
(defthm cst-lexeme-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "comment") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "comment"))))
Theorem:
(defthm cst-lexeme-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "whitespace") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "whitespace"))))
Theorem:
(defthm cst-expression-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "path") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "path"))))
Theorem:
(defthm cst-expression-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "function-call") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "function-call"))))
Theorem:
(defthm cst-expression-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "literal") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "literal"))))
Theorem:
(defthm cst-statement-conc1-matching (implies (cst-list-list-conc-matchp abnf::cstss "block") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "block"))))
Theorem:
(defthm cst-statement-conc2-matching (implies (cst-list-list-conc-matchp abnf::cstss "variable-declaration") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "variable-declaration"))))
Theorem:
(defthm cst-statement-conc3-matching (implies (cst-list-list-conc-matchp abnf::cstss "assignment") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "assignment"))))
Theorem:
(defthm cst-statement-conc4-matching (implies (cst-list-list-conc-matchp abnf::cstss "function-call") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "function-call"))))
Theorem:
(defthm cst-statement-conc5-matching (implies (cst-list-list-conc-matchp abnf::cstss "if-statement") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "if-statement"))))
Theorem:
(defthm cst-statement-conc6-matching (implies (cst-list-list-conc-matchp abnf::cstss "for-statement") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "for-statement"))))
Theorem:
(defthm cst-statement-conc7-matching (implies (cst-list-list-conc-matchp abnf::cstss "switch-statement") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "switch-statement"))))
Theorem:
(defthm cst-statement-conc8-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"leave\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"leave\""))))
Theorem:
(defthm cst-statement-conc9-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"break\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"break\""))))
Theorem:
(defthm cst-statement-conc10-matching (implies (cst-list-list-conc-matchp abnf::cstss "%s\"continue\"") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "%s\"continue\""))))
Theorem:
(defthm cst-statement-conc11-matching (implies (cst-list-list-conc-matchp abnf::cstss "function-definition") (and (equal (len abnf::cstss) 1) (cst-list-rep-matchp (nth 0 abnf::cstss) "function-definition"))))
Theorem:
(defthm cst-boolean-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"true\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"true\""))))
Theorem:
(defthm cst-boolean-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"false\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"false\""))))
Theorem:
(defthm cst-dquote-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-squote-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x27") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x27"))))
Theorem:
(defthm cst-lf-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xA") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xA"))))
Theorem:
(defthm cst-cr-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xD") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xD"))))
Theorem:
(defthm cst-decimal-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-nonzero-decimal-digit-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-hex-digit-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "decimal-digit") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "decimal-digit"))))
Theorem:
(defthm cst-hex-digit-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%i\"a\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%i\"a\""))))
Theorem:
(defthm cst-hex-digit-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "%i\"b\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%i\"b\""))))
Theorem:
(defthm cst-hex-digit-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "%i\"c\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%i\"c\""))))
Theorem:
(defthm cst-hex-digit-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "%i\"d\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%i\"d\""))))
Theorem:
(defthm cst-hex-digit-conc6-rep-matching (implies (cst-list-rep-matchp abnf::csts "%i\"e\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%i\"e\""))))
Theorem:
(defthm cst-hex-digit-conc7-rep-matching (implies (cst-list-rep-matchp abnf::csts "%i\"f\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%i\"f\""))))
Theorem:
(defthm cst-decimal-number-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"0\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"0\""))))
Theorem:
(defthm cst-double-quoted-printable-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-double-quoted-printable-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-double-quoted-printable-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x5D-7E") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x5D-7E"))))
Theorem:
(defthm cst-single-quoted-printable-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x20-26") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x20-26"))))
Theorem:
(defthm cst-single-quoted-printable-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x28-5B") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x28-5B"))))
Theorem:
(defthm cst-single-quoted-printable-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x5D-7E") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x5D-7E"))))
Theorem:
(defthm cst-literal-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "decimal-number") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "decimal-number"))))
Theorem:
(defthm cst-literal-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "hex-number") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "hex-number"))))
Theorem:
(defthm cst-literal-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "boolean") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "boolean"))))
Theorem:
(defthm cst-literal-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "string-literal") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "string-literal"))))
Theorem:
(defthm cst-literal-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "hex-string") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "hex-string"))))
Theorem:
(defthm cst-lowercase-letter-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x61-7A") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x61-7A"))))
Theorem:
(defthm cst-uppercase-letter-conc-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x41-5A") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x41-5A"))))
Theorem:
(defthm cst-identifier-start-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "lowercase-letter") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "lowercase-letter"))))
Theorem:
(defthm cst-identifier-start-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "uppercase-letter") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "uppercase-letter"))))
Theorem:
(defthm cst-identifier-start-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"$\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"$\""))))
Theorem:
(defthm cst-identifier-start-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"_\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"_\""))))
Theorem:
(defthm cst-identifier-rest-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "identifier-start") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "identifier-start"))))
Theorem:
(defthm cst-identifier-rest-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "decimal-digit") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "decimal-digit"))))
Theorem:
(defthm cst-keyword-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"function\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"function\""))))
Theorem:
(defthm cst-keyword-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"if\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"if\""))))
Theorem:
(defthm cst-keyword-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"for\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"for\""))))
Theorem:
(defthm cst-keyword-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"switch\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"switch\""))))
Theorem:
(defthm cst-keyword-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"case\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"case\""))))
Theorem:
(defthm cst-keyword-conc6-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"default\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"default\""))))
Theorem:
(defthm cst-keyword-conc7-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"let\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"let\""))))
Theorem:
(defthm cst-keyword-conc8-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"leave\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"leave\""))))
Theorem:
(defthm cst-keyword-conc9-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"break\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"break\""))))
Theorem:
(defthm cst-keyword-conc10-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"continue\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"continue\""))))
Theorem:
(defthm cst-symbol-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "\".\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\".\""))))
Theorem:
(defthm cst-symbol-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "\",\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\",\""))))
Theorem:
(defthm cst-symbol-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"->\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"->\""))))
Theorem:
(defthm cst-symbol-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"(\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"(\""))))
Theorem:
(defthm cst-symbol-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "\")\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\")\""))))
Theorem:
(defthm cst-symbol-conc6-rep-matching (implies (cst-list-rep-matchp abnf::csts "\":=\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\":=\""))))
Theorem:
(defthm cst-symbol-conc7-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"{\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"{\""))))
Theorem:
(defthm cst-symbol-conc8-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"}\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"}\""))))
Theorem:
(defthm cst-whitespace-char-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x20") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x20"))))
Theorem:
(defthm cst-whitespace-char-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x9") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x9"))))
Theorem:
(defthm cst-whitespace-char-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xD") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xD"))))
Theorem:
(defthm cst-whitespace-char-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xA") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xA"))))
Theorem:
(defthm cst-whitespace-char-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xC") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xC"))))
Theorem:
(defthm cst-not-star-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x0-29") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x0-29"))))
Theorem:
(defthm cst-not-star-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x2B-7F") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x2B-7F"))))
Theorem:
(defthm cst-not-star-or-slash-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x0-29") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x0-29"))))
Theorem:
(defthm cst-not-star-or-slash-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x2B-2E") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x2B-2E"))))
Theorem:
(defthm cst-not-star-or-slash-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x30-7F") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x30-7F"))))
Theorem:
(defthm cst-rest-of-block-comment-after-star-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "\"/\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "\"/\""))))
Theorem:
(defthm cst-not-lf-or-cr-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "%x0-9") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%x0-9"))))
Theorem:
(defthm cst-not-lf-or-cr-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xB-C") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xB-C"))))
Theorem:
(defthm cst-not-lf-or-cr-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "%xE-7F") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%xE-7F"))))
Theorem:
(defthm cst-comment-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "block-comment") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "block-comment"))))
Theorem:
(defthm cst-comment-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "end-of-line-comment") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "end-of-line-comment"))))
Theorem:
(defthm cst-token-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "keyword") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "keyword"))))
Theorem:
(defthm cst-token-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "literal") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "literal"))))
Theorem:
(defthm cst-token-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "identifier") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "identifier"))))
Theorem:
(defthm cst-token-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "symbol") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "symbol"))))
Theorem:
(defthm cst-lexeme-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "token") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "token"))))
Theorem:
(defthm cst-lexeme-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "comment") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "comment"))))
Theorem:
(defthm cst-lexeme-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "whitespace") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "whitespace"))))
Theorem:
(defthm cst-expression-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "path") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "path"))))
Theorem:
(defthm cst-expression-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "function-call") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "function-call"))))
Theorem:
(defthm cst-expression-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "literal") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "literal"))))
Theorem:
(defthm cst-statement-conc1-rep-matching (implies (cst-list-rep-matchp abnf::csts "block") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "block"))))
Theorem:
(defthm cst-statement-conc2-rep-matching (implies (cst-list-rep-matchp abnf::csts "variable-declaration") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "variable-declaration"))))
Theorem:
(defthm cst-statement-conc3-rep-matching (implies (cst-list-rep-matchp abnf::csts "assignment") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "assignment"))))
Theorem:
(defthm cst-statement-conc4-rep-matching (implies (cst-list-rep-matchp abnf::csts "function-call") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "function-call"))))
Theorem:
(defthm cst-statement-conc5-rep-matching (implies (cst-list-rep-matchp abnf::csts "if-statement") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "if-statement"))))
Theorem:
(defthm cst-statement-conc6-rep-matching (implies (cst-list-rep-matchp abnf::csts "for-statement") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "for-statement"))))
Theorem:
(defthm cst-statement-conc7-rep-matching (implies (cst-list-rep-matchp abnf::csts "switch-statement") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "switch-statement"))))
Theorem:
(defthm cst-statement-conc8-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"leave\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"leave\""))))
Theorem:
(defthm cst-statement-conc9-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"break\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"break\""))))
Theorem:
(defthm cst-statement-conc10-rep-matching (implies (cst-list-rep-matchp abnf::csts "%s\"continue\"") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "%s\"continue\""))))
Theorem:
(defthm cst-statement-conc11-rep-matching (implies (cst-list-rep-matchp abnf::csts "function-definition") (and (equal (len abnf::csts) 1) (cst-matchp (nth 0 abnf::csts) "function-definition"))))
Theorem:
(defthm cst-literal-conc-equivs (implies (cst-matchp abnf::cst "literal") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "decimal-number") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "decimal-number"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "hex-number") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "hex-number"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "boolean") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "boolean"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "string-literal") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "string-literal"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "hex-string") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "hex-string"))))))
Theorem:
(defthm cst-identifier-rest-conc-equivs (implies (cst-matchp abnf::cst "identifier-rest") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier-start") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "identifier-start"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "decimal-digit") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "decimal-digit"))))))
Theorem:
(defthm cst-comment-conc-equivs (implies (cst-matchp abnf::cst "comment") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "block-comment") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "block-comment"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "end-of-line-comment") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "end-of-line-comment"))))))
Theorem:
(defthm cst-token-conc-equivs (implies (cst-matchp abnf::cst "token") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "keyword") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "keyword"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "literal") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "literal"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "identifier"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "symbol") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "symbol"))))))
Theorem:
(defthm cst-lexeme-conc-equivs (implies (cst-matchp abnf::cst "lexeme") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "token") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "token"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "comment") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "comment"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "whitespace") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "whitespace"))))))
Theorem:
(defthm cst-expression-conc-equivs (implies (cst-matchp abnf::cst "expression") (and (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "path") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "path"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "function-call") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "function-call"))) (iff (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "literal") (equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "literal"))))))
Function:
(defun cst-literal-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "literal"))) (let ((__function__ 'cst-literal-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "decimal-number")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "hex-number")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "boolean")) 3) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "string-literal")) 4) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "hex-string")) 5) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-literal-conc? (b* ((number (cst-literal-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc?-possibilities (b* ((number (cst-literal-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4) (equal number 5))) :rule-classes ((:forward-chaining :trigger-terms ((cst-literal-conc? abnf::cst)))))
Theorem:
(defthm cst-literal-conc?-of-tree-fix-cst (equal (cst-literal-conc? (abnf::tree-fix abnf::cst)) (cst-literal-conc? abnf::cst)))
Theorem:
(defthm cst-literal-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc? abnf::cst) (cst-literal-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-literal-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "literal") (iff (equal (cst-literal-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "decimal-number"))))
Theorem:
(defthm cst-literal-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "literal") (iff (equal (cst-literal-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "hex-number"))))
Theorem:
(defthm cst-literal-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "literal") (iff (equal (cst-literal-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "boolean"))))
Theorem:
(defthm cst-literal-conc?-4-iff-match-conc (implies (cst-matchp abnf::cst "literal") (iff (equal (cst-literal-conc? abnf::cst) 4) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "string-literal"))))
Theorem:
(defthm cst-literal-conc?-5-iff-match-conc (implies (cst-matchp abnf::cst "literal") (iff (equal (cst-literal-conc? abnf::cst) 5) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "hex-string"))))
Function:
(defun cst-identifier-rest-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "identifier-rest"))) (let ((__function__ 'cst-identifier-rest-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "identifier-start")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "decimal-digit")) 2) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-identifier-rest-conc? (b* ((number (cst-identifier-rest-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc?-possibilities (b* ((number (cst-identifier-rest-conc? abnf::cst))) (or (equal number 1) (equal number 2))) :rule-classes ((:forward-chaining :trigger-terms ((cst-identifier-rest-conc? abnf::cst)))))
Theorem:
(defthm cst-identifier-rest-conc?-of-tree-fix-cst (equal (cst-identifier-rest-conc? (abnf::tree-fix abnf::cst)) (cst-identifier-rest-conc? abnf::cst)))
Theorem:
(defthm cst-identifier-rest-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-rest-conc? abnf::cst) (cst-identifier-rest-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-identifier-rest-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "identifier-rest") (iff (equal (cst-identifier-rest-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier-start"))))
Theorem:
(defthm cst-identifier-rest-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "identifier-rest") (iff (equal (cst-identifier-rest-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "decimal-digit"))))
Function:
(defun cst-comment-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "comment"))) (let ((__function__ 'cst-comment-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "block-comment")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "end-of-line-comment")) 2) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-comment-conc? (b* ((number (cst-comment-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc?-possibilities (b* ((number (cst-comment-conc? abnf::cst))) (or (equal number 1) (equal number 2))) :rule-classes ((:forward-chaining :trigger-terms ((cst-comment-conc? abnf::cst)))))
Theorem:
(defthm cst-comment-conc?-of-tree-fix-cst (equal (cst-comment-conc? (abnf::tree-fix abnf::cst)) (cst-comment-conc? abnf::cst)))
Theorem:
(defthm cst-comment-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-comment-conc? abnf::cst) (cst-comment-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-comment-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "comment") (iff (equal (cst-comment-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "block-comment"))))
Theorem:
(defthm cst-comment-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "comment") (iff (equal (cst-comment-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "end-of-line-comment"))))
Function:
(defun cst-token-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "token"))) (let ((__function__ 'cst-token-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "keyword")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "literal")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "identifier")) 3) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "symbol")) 4) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-token-conc? (b* ((number (cst-token-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc?-possibilities (b* ((number (cst-token-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4))) :rule-classes ((:forward-chaining :trigger-terms ((cst-token-conc? abnf::cst)))))
Theorem:
(defthm cst-token-conc?-of-tree-fix-cst (equal (cst-token-conc? (abnf::tree-fix abnf::cst)) (cst-token-conc? abnf::cst)))
Theorem:
(defthm cst-token-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc? abnf::cst) (cst-token-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-token-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "token") (iff (equal (cst-token-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "keyword"))))
Theorem:
(defthm cst-token-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "token") (iff (equal (cst-token-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "literal"))))
Theorem:
(defthm cst-token-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "token") (iff (equal (cst-token-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "identifier"))))
Theorem:
(defthm cst-token-conc?-4-iff-match-conc (implies (cst-matchp abnf::cst "token") (iff (equal (cst-token-conc? abnf::cst) 4) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "symbol"))))
Function:
(defun cst-lexeme-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lexeme"))) (let ((__function__ 'cst-lexeme-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "token")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "comment")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "whitespace")) 3) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-lexeme-conc? (b* ((number (cst-lexeme-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc?-possibilities (b* ((number (cst-lexeme-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3))) :rule-classes ((:forward-chaining :trigger-terms ((cst-lexeme-conc? abnf::cst)))))
Theorem:
(defthm cst-lexeme-conc?-of-tree-fix-cst (equal (cst-lexeme-conc? (abnf::tree-fix abnf::cst)) (cst-lexeme-conc? abnf::cst)))
Theorem:
(defthm cst-lexeme-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc? abnf::cst) (cst-lexeme-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-lexeme-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "lexeme") (iff (equal (cst-lexeme-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "token"))))
Theorem:
(defthm cst-lexeme-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "lexeme") (iff (equal (cst-lexeme-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "comment"))))
Theorem:
(defthm cst-lexeme-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "lexeme") (iff (equal (cst-lexeme-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "whitespace"))))
Function:
(defun cst-expression-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "expression"))) (let ((__function__ 'cst-expression-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "path")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "function-call")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "literal")) 3) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-cst-expression-conc? (b* ((number (cst-expression-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc?-possibilities (b* ((number (cst-expression-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3))) :rule-classes ((:forward-chaining :trigger-terms ((cst-expression-conc? abnf::cst)))))
Theorem:
(defthm cst-expression-conc?-of-tree-fix-cst (equal (cst-expression-conc? (abnf::tree-fix abnf::cst)) (cst-expression-conc? abnf::cst)))
Theorem:
(defthm cst-expression-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc? abnf::cst) (cst-expression-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-expression-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "expression") (iff (equal (cst-expression-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "path"))))
Theorem:
(defthm cst-expression-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "expression") (iff (equal (cst-expression-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "function-call"))))
Theorem:
(defthm cst-expression-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "expression") (iff (equal (cst-expression-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "literal"))))
Function:
(defun cst-dquote-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "dquote"))) (let ((__function__ 'cst-dquote-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-dquote-conc (b* ((abnf::cstss (cst-dquote-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-dquote-conc-match (implies (cst-matchp abnf::cst "dquote") (b* ((abnf::cstss (cst-dquote-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x22"))) :rule-classes :rewrite)
Theorem:
(defthm cst-dquote-conc-of-tree-fix-cst (equal (cst-dquote-conc (abnf::tree-fix abnf::cst)) (cst-dquote-conc abnf::cst)))
Theorem:
(defthm cst-dquote-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-dquote-conc abnf::cst) (cst-dquote-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-squote-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "squote"))) (let ((__function__ 'cst-squote-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-squote-conc (b* ((abnf::cstss (cst-squote-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-squote-conc-match (implies (cst-matchp abnf::cst "squote") (b* ((abnf::cstss (cst-squote-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x27"))) :rule-classes :rewrite)
Theorem:
(defthm cst-squote-conc-of-tree-fix-cst (equal (cst-squote-conc (abnf::tree-fix abnf::cst)) (cst-squote-conc abnf::cst)))
Theorem:
(defthm cst-squote-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-squote-conc abnf::cst) (cst-squote-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lf-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lf"))) (let ((__function__ 'cst-lf-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-lf-conc (b* ((abnf::cstss (cst-lf-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-lf-conc-match (implies (cst-matchp abnf::cst "lf") (b* ((abnf::cstss (cst-lf-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%xA"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lf-conc-of-tree-fix-cst (equal (cst-lf-conc (abnf::tree-fix abnf::cst)) (cst-lf-conc abnf::cst)))
Theorem:
(defthm cst-lf-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lf-conc abnf::cst) (cst-lf-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-cr-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "cr"))) (let ((__function__ 'cst-cr-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-cr-conc (b* ((abnf::cstss (cst-cr-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-cr-conc-match (implies (cst-matchp abnf::cst "cr") (b* ((abnf::cstss (cst-cr-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%xD"))) :rule-classes :rewrite)
Theorem:
(defthm cst-cr-conc-of-tree-fix-cst (equal (cst-cr-conc (abnf::tree-fix abnf::cst)) (cst-cr-conc abnf::cst)))
Theorem:
(defthm cst-cr-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-cr-conc abnf::cst) (cst-cr-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-decimal-digit-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "decimal-digit"))) (let ((__function__ 'cst-decimal-digit-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-decimal-digit-conc (b* ((abnf::cstss (cst-decimal-digit-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-digit-conc-match (implies (cst-matchp abnf::cst "decimal-digit") (b* ((abnf::cstss (cst-decimal-digit-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-digit-conc-of-tree-fix-cst (equal (cst-decimal-digit-conc (abnf::tree-fix abnf::cst)) (cst-decimal-digit-conc abnf::cst)))
Theorem:
(defthm cst-decimal-digit-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-decimal-digit-conc abnf::cst) (cst-decimal-digit-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-nonzero-decimal-digit-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "nonzero-decimal-digit"))) (let ((__function__ 'cst-nonzero-decimal-digit-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-nonzero-decimal-digit-conc (b* ((abnf::cstss (cst-nonzero-decimal-digit-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-nonzero-decimal-digit-conc-match (implies (cst-matchp abnf::cst "nonzero-decimal-digit") (b* ((abnf::cstss (cst-nonzero-decimal-digit-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x31-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-nonzero-decimal-digit-conc-of-tree-fix-cst (equal (cst-nonzero-decimal-digit-conc (abnf::tree-fix abnf::cst)) (cst-nonzero-decimal-digit-conc abnf::cst)))
Theorem:
(defthm cst-nonzero-decimal-digit-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-nonzero-decimal-digit-conc abnf::cst) (cst-nonzero-decimal-digit-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-hex-number-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "hex-number"))) (let ((__function__ 'cst-hex-number-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-hex-number-conc (b* ((abnf::cstss (cst-hex-number-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-hex-number-conc-match (implies (cst-matchp abnf::cst "hex-number") (b* ((abnf::cstss (cst-hex-number-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%s\"0x\" *hex-digit"))) :rule-classes :rewrite)
Theorem:
(defthm cst-hex-number-conc-of-tree-fix-cst (equal (cst-hex-number-conc (abnf::tree-fix abnf::cst)) (cst-hex-number-conc abnf::cst)))
Theorem:
(defthm cst-hex-number-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-hex-number-conc abnf::cst) (cst-hex-number-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-hex-string-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "hex-string"))) (let ((__function__ 'cst-hex-string-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-hex-string-conc (b* ((abnf::cstss (cst-hex-string-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-hex-string-conc-match (implies (cst-matchp abnf::cst "hex-string") (b* ((abnf::cstss (cst-hex-string-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%s\"hex\" ( dquote [ 2hex-digit *( [ \"_\" ] 2hex-digit ) ] dquote / squote [ 2hex-digit *( [ \"_\" ] 2hex-digit ) ] squote )"))) :rule-classes :rewrite)
Theorem:
(defthm cst-hex-string-conc-of-tree-fix-cst (equal (cst-hex-string-conc (abnf::tree-fix abnf::cst)) (cst-hex-string-conc abnf::cst)))
Theorem:
(defthm cst-hex-string-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-hex-string-conc abnf::cst) (cst-hex-string-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-escape-sequence-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "escape-sequence"))) (let ((__function__ 'cst-escape-sequence-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-escape-sequence-conc (b* ((abnf::cstss (cst-escape-sequence-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-escape-sequence-conc-match (implies (cst-matchp abnf::cst "escape-sequence") (b* ((abnf::cstss (cst-escape-sequence-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "\"\\\" ( ( squote / dquote / %s\"\\\" / %s\"n\" / %s\"r\" / %s\"t\" / lf / cr ) / %s\"u\" 4hex-digit / %s\"x\" 2hex-digit )"))) :rule-classes :rewrite)
Theorem:
(defthm cst-escape-sequence-conc-of-tree-fix-cst (equal (cst-escape-sequence-conc (abnf::tree-fix abnf::cst)) (cst-escape-sequence-conc abnf::cst)))
Theorem:
(defthm cst-escape-sequence-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-escape-sequence-conc abnf::cst) (cst-escape-sequence-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 1)))) (let ((__function__ 'cst-literal-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-literal-conc1 (b* ((abnf::cstss (cst-literal-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc1-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-literal-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "decimal-number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc1-of-tree-fix-cst (equal (cst-literal-conc1 (abnf::tree-fix abnf::cst)) (cst-literal-conc1 abnf::cst)))
Theorem:
(defthm cst-literal-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc1 abnf::cst) (cst-literal-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 2)))) (let ((__function__ 'cst-literal-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-literal-conc2 (b* ((abnf::cstss (cst-literal-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc2-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-literal-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "hex-number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc2-of-tree-fix-cst (equal (cst-literal-conc2 (abnf::tree-fix abnf::cst)) (cst-literal-conc2 abnf::cst)))
Theorem:
(defthm cst-literal-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc2 abnf::cst) (cst-literal-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc3 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 3)))) (let ((__function__ 'cst-literal-conc3)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-literal-conc3 (b* ((abnf::cstss (cst-literal-conc3 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc3-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 3)) (b* ((abnf::cstss (cst-literal-conc3 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "boolean"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc3-of-tree-fix-cst (equal (cst-literal-conc3 (abnf::tree-fix abnf::cst)) (cst-literal-conc3 abnf::cst)))
Theorem:
(defthm cst-literal-conc3-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc3 abnf::cst) (cst-literal-conc3 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc4 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 4)))) (let ((__function__ 'cst-literal-conc4)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-literal-conc4 (b* ((abnf::cstss (cst-literal-conc4 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc4-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 4)) (b* ((abnf::cstss (cst-literal-conc4 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "string-literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc4-of-tree-fix-cst (equal (cst-literal-conc4 (abnf::tree-fix abnf::cst)) (cst-literal-conc4 abnf::cst)))
Theorem:
(defthm cst-literal-conc4-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc4 abnf::cst) (cst-literal-conc4 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc5 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 5)))) (let ((__function__ 'cst-literal-conc5)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-literal-conc5 (b* ((abnf::cstss (cst-literal-conc5 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc5-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 5)) (b* ((abnf::cstss (cst-literal-conc5 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "hex-string"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc5-of-tree-fix-cst (equal (cst-literal-conc5 (abnf::tree-fix abnf::cst)) (cst-literal-conc5 abnf::cst)))
Theorem:
(defthm cst-literal-conc5-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc5 abnf::cst) (cst-literal-conc5 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lowercase-letter-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lowercase-letter"))) (let ((__function__ 'cst-lowercase-letter-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-lowercase-letter-conc (b* ((abnf::cstss (cst-lowercase-letter-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-match (implies (cst-matchp abnf::cst "lowercase-letter") (b* ((abnf::cstss (cst-lowercase-letter-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x61-7A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-of-tree-fix-cst (equal (cst-lowercase-letter-conc (abnf::tree-fix abnf::cst)) (cst-lowercase-letter-conc abnf::cst)))
Theorem:
(defthm cst-lowercase-letter-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lowercase-letter-conc abnf::cst) (cst-lowercase-letter-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-uppercase-letter-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "uppercase-letter"))) (let ((__function__ 'cst-uppercase-letter-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-uppercase-letter-conc (b* ((abnf::cstss (cst-uppercase-letter-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-match (implies (cst-matchp abnf::cst "uppercase-letter") (b* ((abnf::cstss (cst-uppercase-letter-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%x41-5A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-of-tree-fix-cst (equal (cst-uppercase-letter-conc (abnf::tree-fix abnf::cst)) (cst-uppercase-letter-conc abnf::cst)))
Theorem:
(defthm cst-uppercase-letter-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-uppercase-letter-conc abnf::cst) (cst-uppercase-letter-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-identifier-rest-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 1)))) (let ((__function__ 'cst-identifier-rest-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-identifier-rest-conc1 (b* ((abnf::cstss (cst-identifier-rest-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc1-match (implies (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-identifier-rest-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "identifier-start"))) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc1-of-tree-fix-cst (equal (cst-identifier-rest-conc1 (abnf::tree-fix abnf::cst)) (cst-identifier-rest-conc1 abnf::cst)))
Theorem:
(defthm cst-identifier-rest-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-rest-conc1 abnf::cst) (cst-identifier-rest-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-identifier-rest-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 2)))) (let ((__function__ 'cst-identifier-rest-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-identifier-rest-conc2 (b* ((abnf::cstss (cst-identifier-rest-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc2-match (implies (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-identifier-rest-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "decimal-digit"))) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc2-of-tree-fix-cst (equal (cst-identifier-rest-conc2 (abnf::tree-fix abnf::cst)) (cst-identifier-rest-conc2 abnf::cst)))
Theorem:
(defthm cst-identifier-rest-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-rest-conc2 abnf::cst) (cst-identifier-rest-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-identifier-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "identifier"))) (let ((__function__ 'cst-identifier-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-identifier-conc (b* ((abnf::cstss (cst-identifier-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-conc-match (implies (cst-matchp abnf::cst "identifier") (b* ((abnf::cstss (cst-identifier-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "identifier-start *identifier-rest"))) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-conc-of-tree-fix-cst (equal (cst-identifier-conc (abnf::tree-fix abnf::cst)) (cst-identifier-conc abnf::cst)))
Theorem:
(defthm cst-identifier-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-conc abnf::cst) (cst-identifier-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-whitespace-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "whitespace"))) (let ((__function__ 'cst-whitespace-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-whitespace-conc (b* ((abnf::cstss (cst-whitespace-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc-match (implies (cst-matchp abnf::cst "whitespace") (b* ((abnf::cstss (cst-whitespace-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "1*whitespace-char"))) :rule-classes :rewrite)
Theorem:
(defthm cst-whitespace-conc-of-tree-fix-cst (equal (cst-whitespace-conc (abnf::tree-fix abnf::cst)) (cst-whitespace-conc abnf::cst)))
Theorem:
(defthm cst-whitespace-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-whitespace-conc abnf::cst) (cst-whitespace-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-block-comment-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "block-comment"))) (let ((__function__ 'cst-block-comment-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-block-comment-conc (b* ((abnf::cstss (cst-block-comment-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-block-comment-conc-match (implies (cst-matchp abnf::cst "block-comment") (b* ((abnf::cstss (cst-block-comment-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "\"/*\" rest-of-block-comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-block-comment-conc-of-tree-fix-cst (equal (cst-block-comment-conc (abnf::tree-fix abnf::cst)) (cst-block-comment-conc abnf::cst)))
Theorem:
(defthm cst-block-comment-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-block-comment-conc abnf::cst) (cst-block-comment-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-end-of-line-comment-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "end-of-line-comment"))) (let ((__function__ 'cst-end-of-line-comment-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-end-of-line-comment-conc (b* ((abnf::cstss (cst-end-of-line-comment-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-end-of-line-comment-conc-match (implies (cst-matchp abnf::cst "end-of-line-comment") (b* ((abnf::cstss (cst-end-of-line-comment-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "\"//\" *not-lf-or-cr"))) :rule-classes :rewrite)
Theorem:
(defthm cst-end-of-line-comment-conc-of-tree-fix-cst (equal (cst-end-of-line-comment-conc (abnf::tree-fix abnf::cst)) (cst-end-of-line-comment-conc abnf::cst)))
Theorem:
(defthm cst-end-of-line-comment-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-end-of-line-comment-conc abnf::cst) (cst-end-of-line-comment-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-comment-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 1)))) (let ((__function__ 'cst-comment-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-comment-conc1 (b* ((abnf::cstss (cst-comment-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc1-match (implies (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-comment-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "block-comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc1-of-tree-fix-cst (equal (cst-comment-conc1 (abnf::tree-fix abnf::cst)) (cst-comment-conc1 abnf::cst)))
Theorem:
(defthm cst-comment-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-comment-conc1 abnf::cst) (cst-comment-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-comment-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 2)))) (let ((__function__ 'cst-comment-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-comment-conc2 (b* ((abnf::cstss (cst-comment-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc2-match (implies (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-comment-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "end-of-line-comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc2-of-tree-fix-cst (equal (cst-comment-conc2 (abnf::tree-fix abnf::cst)) (cst-comment-conc2 abnf::cst)))
Theorem:
(defthm cst-comment-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-comment-conc2 abnf::cst) (cst-comment-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)))) (let ((__function__ 'cst-token-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-token-conc1 (b* ((abnf::cstss (cst-token-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-token-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "keyword"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-of-tree-fix-cst (equal (cst-token-conc1 (abnf::tree-fix abnf::cst)) (cst-token-conc1 abnf::cst)))
Theorem:
(defthm cst-token-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc1 abnf::cst) (cst-token-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)))) (let ((__function__ 'cst-token-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-token-conc2 (b* ((abnf::cstss (cst-token-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-token-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-of-tree-fix-cst (equal (cst-token-conc2 (abnf::tree-fix abnf::cst)) (cst-token-conc2 abnf::cst)))
Theorem:
(defthm cst-token-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc2 abnf::cst) (cst-token-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc3 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)))) (let ((__function__ 'cst-token-conc3)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-token-conc3 (b* ((abnf::cstss (cst-token-conc3 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)) (b* ((abnf::cstss (cst-token-conc3 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "identifier"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-of-tree-fix-cst (equal (cst-token-conc3 (abnf::tree-fix abnf::cst)) (cst-token-conc3 abnf::cst)))
Theorem:
(defthm cst-token-conc3-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc3 abnf::cst) (cst-token-conc3 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc4 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)))) (let ((__function__ 'cst-token-conc4)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-token-conc4 (b* ((abnf::cstss (cst-token-conc4 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)) (b* ((abnf::cstss (cst-token-conc4 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "symbol"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-of-tree-fix-cst (equal (cst-token-conc4 (abnf::tree-fix abnf::cst)) (cst-token-conc4 abnf::cst)))
Theorem:
(defthm cst-token-conc4-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc4 abnf::cst) (cst-token-conc4 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)))) (let ((__function__ 'cst-lexeme-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-lexeme-conc1 (b* ((abnf::cstss (cst-lexeme-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-lexeme-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "token"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-of-tree-fix-cst (equal (cst-lexeme-conc1 (abnf::tree-fix abnf::cst)) (cst-lexeme-conc1 abnf::cst)))
Theorem:
(defthm cst-lexeme-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc1 abnf::cst) (cst-lexeme-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)))) (let ((__function__ 'cst-lexeme-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-lexeme-conc2 (b* ((abnf::cstss (cst-lexeme-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-lexeme-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-of-tree-fix-cst (equal (cst-lexeme-conc2 (abnf::tree-fix abnf::cst)) (cst-lexeme-conc2 abnf::cst)))
Theorem:
(defthm cst-lexeme-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc2 abnf::cst) (cst-lexeme-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc3 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 3)))) (let ((__function__ 'cst-lexeme-conc3)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-lexeme-conc3 (b* ((abnf::cstss (cst-lexeme-conc3 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc3-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 3)) (b* ((abnf::cstss (cst-lexeme-conc3 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "whitespace"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc3-of-tree-fix-cst (equal (cst-lexeme-conc3 (abnf::tree-fix abnf::cst)) (cst-lexeme-conc3 abnf::cst)))
Theorem:
(defthm cst-lexeme-conc3-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc3 abnf::cst) (cst-lexeme-conc3 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-path-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "path"))) (let ((__function__ 'cst-path-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-path-conc (b* ((abnf::cstss (cst-path-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-path-conc-match (implies (cst-matchp abnf::cst "path") (b* ((abnf::cstss (cst-path-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "identifier *( \".\" identifier )"))) :rule-classes :rewrite)
Theorem:
(defthm cst-path-conc-of-tree-fix-cst (equal (cst-path-conc (abnf::tree-fix abnf::cst)) (cst-path-conc abnf::cst)))
Theorem:
(defthm cst-path-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-path-conc abnf::cst) (cst-path-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc1 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 1)))) (let ((__function__ 'cst-expression-conc1)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-expression-conc1 (b* ((abnf::cstss (cst-expression-conc1 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc1-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 1)) (b* ((abnf::cstss (cst-expression-conc1 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "path"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc1-of-tree-fix-cst (equal (cst-expression-conc1 (abnf::tree-fix abnf::cst)) (cst-expression-conc1 abnf::cst)))
Theorem:
(defthm cst-expression-conc1-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc1 abnf::cst) (cst-expression-conc1 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc2 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 2)))) (let ((__function__ 'cst-expression-conc2)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-expression-conc2 (b* ((abnf::cstss (cst-expression-conc2 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc2-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 2)) (b* ((abnf::cstss (cst-expression-conc2 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "function-call"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc2-of-tree-fix-cst (equal (cst-expression-conc2 (abnf::tree-fix abnf::cst)) (cst-expression-conc2 abnf::cst)))
Theorem:
(defthm cst-expression-conc2-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc2 abnf::cst) (cst-expression-conc2 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc3 (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 3)))) (let ((__function__ 'cst-expression-conc3)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-expression-conc3 (b* ((abnf::cstss (cst-expression-conc3 abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc3-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 3)) (b* ((abnf::cstss (cst-expression-conc3 abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc3-of-tree-fix-cst (equal (cst-expression-conc3 (abnf::tree-fix abnf::cst)) (cst-expression-conc3 abnf::cst)))
Theorem:
(defthm cst-expression-conc3-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc3 abnf::cst) (cst-expression-conc3 cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-function-call-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "function-call"))) (let ((__function__ 'cst-function-call-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-function-call-conc (b* ((abnf::cstss (cst-function-call-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-function-call-conc-match (implies (cst-matchp abnf::cst "function-call") (b* ((abnf::cstss (cst-function-call-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "identifier \"(\" [ expression *( \",\" expression ) ] \")\""))) :rule-classes :rewrite)
Theorem:
(defthm cst-function-call-conc-of-tree-fix-cst (equal (cst-function-call-conc (abnf::tree-fix abnf::cst)) (cst-function-call-conc abnf::cst)))
Theorem:
(defthm cst-function-call-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-function-call-conc abnf::cst) (cst-function-call-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-function-definition-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "function-definition"))) (let ((__function__ 'cst-function-definition-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-function-definition-conc (b* ((abnf::cstss (cst-function-definition-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-function-definition-conc-match (implies (cst-matchp abnf::cst "function-definition") (b* ((abnf::cstss (cst-function-definition-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%s\"function\" identifier \"(\" [ identifier *( \",\" identifier ) ] \")\" [ \"->\" identifier *( \",\" identifier ) ] block"))) :rule-classes :rewrite)
Theorem:
(defthm cst-function-definition-conc-of-tree-fix-cst (equal (cst-function-definition-conc (abnf::tree-fix abnf::cst)) (cst-function-definition-conc abnf::cst)))
Theorem:
(defthm cst-function-definition-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-function-definition-conc abnf::cst) (cst-function-definition-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-if-statement-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "if-statement"))) (let ((__function__ 'cst-if-statement-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-if-statement-conc (b* ((abnf::cstss (cst-if-statement-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-if-statement-conc-match (implies (cst-matchp abnf::cst "if-statement") (b* ((abnf::cstss (cst-if-statement-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%s\"if\" expression block"))) :rule-classes :rewrite)
Theorem:
(defthm cst-if-statement-conc-of-tree-fix-cst (equal (cst-if-statement-conc (abnf::tree-fix abnf::cst)) (cst-if-statement-conc abnf::cst)))
Theorem:
(defthm cst-if-statement-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-if-statement-conc abnf::cst) (cst-if-statement-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-for-statement-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "for-statement"))) (let ((__function__ 'cst-for-statement-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-for-statement-conc (b* ((abnf::cstss (cst-for-statement-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-for-statement-conc-match (implies (cst-matchp abnf::cst "for-statement") (b* ((abnf::cstss (cst-for-statement-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%s\"for\" block expression block block"))) :rule-classes :rewrite)
Theorem:
(defthm cst-for-statement-conc-of-tree-fix-cst (equal (cst-for-statement-conc (abnf::tree-fix abnf::cst)) (cst-for-statement-conc abnf::cst)))
Theorem:
(defthm cst-for-statement-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-for-statement-conc abnf::cst) (cst-for-statement-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-switch-statement-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "switch-statement"))) (let ((__function__ 'cst-switch-statement-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-switch-statement-conc (b* ((abnf::cstss (cst-switch-statement-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-switch-statement-conc-match (implies (cst-matchp abnf::cst "switch-statement") (b* ((abnf::cstss (cst-switch-statement-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "%s\"switch\" expression ( 1*( %s\"case\" literal block ) [ %s\"default\" block ] / %s\"default\" block )"))) :rule-classes :rewrite)
Theorem:
(defthm cst-switch-statement-conc-of-tree-fix-cst (equal (cst-switch-statement-conc (abnf::tree-fix abnf::cst)) (cst-switch-statement-conc abnf::cst)))
Theorem:
(defthm cst-switch-statement-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-switch-statement-conc abnf::cst) (cst-switch-statement-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-block-conc (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "block"))) (let ((__function__ 'cst-block-conc)) (declare (ignorable __function__)) (abnf::tree-nonleaf->branches abnf::cst)))
Theorem:
(defthm tree-list-listp-of-cst-block-conc (b* ((abnf::cstss (cst-block-conc abnf::cst))) (abnf::tree-list-listp abnf::cstss)) :rule-classes :rewrite)
Theorem:
(defthm cst-block-conc-match (implies (cst-matchp abnf::cst "block") (b* ((abnf::cstss (cst-block-conc abnf::cst))) (cst-list-list-conc-matchp abnf::cstss "\"{\" *statement \"}\""))) :rule-classes :rewrite)
Theorem:
(defthm cst-block-conc-of-tree-fix-cst (equal (cst-block-conc (abnf::tree-fix abnf::cst)) (cst-block-conc abnf::cst)))
Theorem:
(defthm cst-block-conc-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-block-conc abnf::cst) (cst-block-conc cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-dquote-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "dquote"))) (let ((__function__ 'cst-dquote-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-dquote-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-dquote-conc-rep (b* ((abnf::csts (cst-dquote-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-dquote-conc-rep-match (implies (cst-matchp abnf::cst "dquote") (b* ((abnf::csts (cst-dquote-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x22"))) :rule-classes :rewrite)
Theorem:
(defthm cst-dquote-conc-rep-of-tree-fix-cst (equal (cst-dquote-conc-rep (abnf::tree-fix abnf::cst)) (cst-dquote-conc-rep abnf::cst)))
Theorem:
(defthm cst-dquote-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-dquote-conc-rep abnf::cst) (cst-dquote-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-squote-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "squote"))) (let ((__function__ 'cst-squote-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-squote-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-squote-conc-rep (b* ((abnf::csts (cst-squote-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-squote-conc-rep-match (implies (cst-matchp abnf::cst "squote") (b* ((abnf::csts (cst-squote-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x27"))) :rule-classes :rewrite)
Theorem:
(defthm cst-squote-conc-rep-of-tree-fix-cst (equal (cst-squote-conc-rep (abnf::tree-fix abnf::cst)) (cst-squote-conc-rep abnf::cst)))
Theorem:
(defthm cst-squote-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-squote-conc-rep abnf::cst) (cst-squote-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lf-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lf"))) (let ((__function__ 'cst-lf-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-lf-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-lf-conc-rep (b* ((abnf::csts (cst-lf-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-lf-conc-rep-match (implies (cst-matchp abnf::cst "lf") (b* ((abnf::csts (cst-lf-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%xA"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lf-conc-rep-of-tree-fix-cst (equal (cst-lf-conc-rep (abnf::tree-fix abnf::cst)) (cst-lf-conc-rep abnf::cst)))
Theorem:
(defthm cst-lf-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lf-conc-rep abnf::cst) (cst-lf-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-cr-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "cr"))) (let ((__function__ 'cst-cr-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-cr-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-cr-conc-rep (b* ((abnf::csts (cst-cr-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-cr-conc-rep-match (implies (cst-matchp abnf::cst "cr") (b* ((abnf::csts (cst-cr-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%xD"))) :rule-classes :rewrite)
Theorem:
(defthm cst-cr-conc-rep-of-tree-fix-cst (equal (cst-cr-conc-rep (abnf::tree-fix abnf::cst)) (cst-cr-conc-rep abnf::cst)))
Theorem:
(defthm cst-cr-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-cr-conc-rep abnf::cst) (cst-cr-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-decimal-digit-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "decimal-digit"))) (let ((__function__ 'cst-decimal-digit-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-decimal-digit-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-decimal-digit-conc-rep (b* ((abnf::csts (cst-decimal-digit-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-digit-conc-rep-match (implies (cst-matchp abnf::cst "decimal-digit") (b* ((abnf::csts (cst-decimal-digit-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-digit-conc-rep-of-tree-fix-cst (equal (cst-decimal-digit-conc-rep (abnf::tree-fix abnf::cst)) (cst-decimal-digit-conc-rep abnf::cst)))
Theorem:
(defthm cst-decimal-digit-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-decimal-digit-conc-rep abnf::cst) (cst-decimal-digit-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-nonzero-decimal-digit-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "nonzero-decimal-digit"))) (let ((__function__ 'cst-nonzero-decimal-digit-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-nonzero-decimal-digit-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-nonzero-decimal-digit-conc-rep (b* ((abnf::csts (cst-nonzero-decimal-digit-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-nonzero-decimal-digit-conc-rep-match (implies (cst-matchp abnf::cst "nonzero-decimal-digit") (b* ((abnf::csts (cst-nonzero-decimal-digit-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x31-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-nonzero-decimal-digit-conc-rep-of-tree-fix-cst (equal (cst-nonzero-decimal-digit-conc-rep (abnf::tree-fix abnf::cst)) (cst-nonzero-decimal-digit-conc-rep abnf::cst)))
Theorem:
(defthm cst-nonzero-decimal-digit-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-nonzero-decimal-digit-conc-rep abnf::cst) (cst-nonzero-decimal-digit-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 1)))) (let ((__function__ 'cst-literal-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-literal-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-literal-conc1-rep (b* ((abnf::csts (cst-literal-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc1-rep-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-literal-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "decimal-number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc1-rep-of-tree-fix-cst (equal (cst-literal-conc1-rep (abnf::tree-fix abnf::cst)) (cst-literal-conc1-rep abnf::cst)))
Theorem:
(defthm cst-literal-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc1-rep abnf::cst) (cst-literal-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 2)))) (let ((__function__ 'cst-literal-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-literal-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-literal-conc2-rep (b* ((abnf::csts (cst-literal-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc2-rep-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-literal-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "hex-number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc2-rep-of-tree-fix-cst (equal (cst-literal-conc2-rep (abnf::tree-fix abnf::cst)) (cst-literal-conc2-rep abnf::cst)))
Theorem:
(defthm cst-literal-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc2-rep abnf::cst) (cst-literal-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc3-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 3)))) (let ((__function__ 'cst-literal-conc3-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-literal-conc3 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-literal-conc3-rep (b* ((abnf::csts (cst-literal-conc3-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc3-rep-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 3)) (b* ((abnf::csts (cst-literal-conc3-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "boolean"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc3-rep-of-tree-fix-cst (equal (cst-literal-conc3-rep (abnf::tree-fix abnf::cst)) (cst-literal-conc3-rep abnf::cst)))
Theorem:
(defthm cst-literal-conc3-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc3-rep abnf::cst) (cst-literal-conc3-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc4-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 4)))) (let ((__function__ 'cst-literal-conc4-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-literal-conc4 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-literal-conc4-rep (b* ((abnf::csts (cst-literal-conc4-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc4-rep-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 4)) (b* ((abnf::csts (cst-literal-conc4-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "string-literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc4-rep-of-tree-fix-cst (equal (cst-literal-conc4-rep (abnf::tree-fix abnf::cst)) (cst-literal-conc4-rep abnf::cst)))
Theorem:
(defthm cst-literal-conc4-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc4-rep abnf::cst) (cst-literal-conc4-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc5-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 5)))) (let ((__function__ 'cst-literal-conc5-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-literal-conc5 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-literal-conc5-rep (b* ((abnf::csts (cst-literal-conc5-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc5-rep-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 5)) (b* ((abnf::csts (cst-literal-conc5-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "hex-string"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc5-rep-of-tree-fix-cst (equal (cst-literal-conc5-rep (abnf::tree-fix abnf::cst)) (cst-literal-conc5-rep abnf::cst)))
Theorem:
(defthm cst-literal-conc5-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc5-rep abnf::cst) (cst-literal-conc5-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lowercase-letter-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lowercase-letter"))) (let ((__function__ 'cst-lowercase-letter-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-lowercase-letter-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-lowercase-letter-conc-rep (b* ((abnf::csts (cst-lowercase-letter-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-rep-match (implies (cst-matchp abnf::cst "lowercase-letter") (b* ((abnf::csts (cst-lowercase-letter-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x61-7A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-rep-of-tree-fix-cst (equal (cst-lowercase-letter-conc-rep (abnf::tree-fix abnf::cst)) (cst-lowercase-letter-conc-rep abnf::cst)))
Theorem:
(defthm cst-lowercase-letter-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lowercase-letter-conc-rep abnf::cst) (cst-lowercase-letter-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-uppercase-letter-conc-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "uppercase-letter"))) (let ((__function__ 'cst-uppercase-letter-conc-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-uppercase-letter-conc abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-uppercase-letter-conc-rep (b* ((abnf::csts (cst-uppercase-letter-conc-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-rep-match (implies (cst-matchp abnf::cst "uppercase-letter") (b* ((abnf::csts (cst-uppercase-letter-conc-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "%x41-5A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-rep-of-tree-fix-cst (equal (cst-uppercase-letter-conc-rep (abnf::tree-fix abnf::cst)) (cst-uppercase-letter-conc-rep abnf::cst)))
Theorem:
(defthm cst-uppercase-letter-conc-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-uppercase-letter-conc-rep abnf::cst) (cst-uppercase-letter-conc-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-identifier-rest-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 1)))) (let ((__function__ 'cst-identifier-rest-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-identifier-rest-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-identifier-rest-conc1-rep (b* ((abnf::csts (cst-identifier-rest-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc1-rep-match (implies (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-identifier-rest-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "identifier-start"))) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc1-rep-of-tree-fix-cst (equal (cst-identifier-rest-conc1-rep (abnf::tree-fix abnf::cst)) (cst-identifier-rest-conc1-rep abnf::cst)))
Theorem:
(defthm cst-identifier-rest-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-rest-conc1-rep abnf::cst) (cst-identifier-rest-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-identifier-rest-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 2)))) (let ((__function__ 'cst-identifier-rest-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-identifier-rest-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-identifier-rest-conc2-rep (b* ((abnf::csts (cst-identifier-rest-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc2-rep-match (implies (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-identifier-rest-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "decimal-digit"))) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc2-rep-of-tree-fix-cst (equal (cst-identifier-rest-conc2-rep (abnf::tree-fix abnf::cst)) (cst-identifier-rest-conc2-rep abnf::cst)))
Theorem:
(defthm cst-identifier-rest-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-rest-conc2-rep abnf::cst) (cst-identifier-rest-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-comment-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 1)))) (let ((__function__ 'cst-comment-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-comment-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-comment-conc1-rep (b* ((abnf::csts (cst-comment-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc1-rep-match (implies (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-comment-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "block-comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc1-rep-of-tree-fix-cst (equal (cst-comment-conc1-rep (abnf::tree-fix abnf::cst)) (cst-comment-conc1-rep abnf::cst)))
Theorem:
(defthm cst-comment-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-comment-conc1-rep abnf::cst) (cst-comment-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-comment-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 2)))) (let ((__function__ 'cst-comment-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-comment-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-comment-conc2-rep (b* ((abnf::csts (cst-comment-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc2-rep-match (implies (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-comment-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "end-of-line-comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc2-rep-of-tree-fix-cst (equal (cst-comment-conc2-rep (abnf::tree-fix abnf::cst)) (cst-comment-conc2-rep abnf::cst)))
Theorem:
(defthm cst-comment-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-comment-conc2-rep abnf::cst) (cst-comment-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)))) (let ((__function__ 'cst-token-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-token-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-token-conc1-rep (b* ((abnf::csts (cst-token-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-rep-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-token-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "keyword"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-rep-of-tree-fix-cst (equal (cst-token-conc1-rep (abnf::tree-fix abnf::cst)) (cst-token-conc1-rep abnf::cst)))
Theorem:
(defthm cst-token-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc1-rep abnf::cst) (cst-token-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)))) (let ((__function__ 'cst-token-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-token-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-token-conc2-rep (b* ((abnf::csts (cst-token-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-rep-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-token-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-rep-of-tree-fix-cst (equal (cst-token-conc2-rep (abnf::tree-fix abnf::cst)) (cst-token-conc2-rep abnf::cst)))
Theorem:
(defthm cst-token-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc2-rep abnf::cst) (cst-token-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc3-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)))) (let ((__function__ 'cst-token-conc3-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-token-conc3 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-token-conc3-rep (b* ((abnf::csts (cst-token-conc3-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-rep-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)) (b* ((abnf::csts (cst-token-conc3-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "identifier"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-rep-of-tree-fix-cst (equal (cst-token-conc3-rep (abnf::tree-fix abnf::cst)) (cst-token-conc3-rep abnf::cst)))
Theorem:
(defthm cst-token-conc3-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc3-rep abnf::cst) (cst-token-conc3-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc4-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)))) (let ((__function__ 'cst-token-conc4-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-token-conc4 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-token-conc4-rep (b* ((abnf::csts (cst-token-conc4-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-rep-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)) (b* ((abnf::csts (cst-token-conc4-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "symbol"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-rep-of-tree-fix-cst (equal (cst-token-conc4-rep (abnf::tree-fix abnf::cst)) (cst-token-conc4-rep abnf::cst)))
Theorem:
(defthm cst-token-conc4-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc4-rep abnf::cst) (cst-token-conc4-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)))) (let ((__function__ 'cst-lexeme-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-lexeme-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-lexeme-conc1-rep (b* ((abnf::csts (cst-lexeme-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-rep-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-lexeme-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "token"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-rep-of-tree-fix-cst (equal (cst-lexeme-conc1-rep (abnf::tree-fix abnf::cst)) (cst-lexeme-conc1-rep abnf::cst)))
Theorem:
(defthm cst-lexeme-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc1-rep abnf::cst) (cst-lexeme-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)))) (let ((__function__ 'cst-lexeme-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-lexeme-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-lexeme-conc2-rep (b* ((abnf::csts (cst-lexeme-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-rep-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-lexeme-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-rep-of-tree-fix-cst (equal (cst-lexeme-conc2-rep (abnf::tree-fix abnf::cst)) (cst-lexeme-conc2-rep abnf::cst)))
Theorem:
(defthm cst-lexeme-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc2-rep abnf::cst) (cst-lexeme-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc3-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 3)))) (let ((__function__ 'cst-lexeme-conc3-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-lexeme-conc3 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-lexeme-conc3-rep (b* ((abnf::csts (cst-lexeme-conc3-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc3-rep-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 3)) (b* ((abnf::csts (cst-lexeme-conc3-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "whitespace"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc3-rep-of-tree-fix-cst (equal (cst-lexeme-conc3-rep (abnf::tree-fix abnf::cst)) (cst-lexeme-conc3-rep abnf::cst)))
Theorem:
(defthm cst-lexeme-conc3-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc3-rep abnf::cst) (cst-lexeme-conc3-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc1-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 1)))) (let ((__function__ 'cst-expression-conc1-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-expression-conc1 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-expression-conc1-rep (b* ((abnf::csts (cst-expression-conc1-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc1-rep-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 1)) (b* ((abnf::csts (cst-expression-conc1-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "path"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc1-rep-of-tree-fix-cst (equal (cst-expression-conc1-rep (abnf::tree-fix abnf::cst)) (cst-expression-conc1-rep abnf::cst)))
Theorem:
(defthm cst-expression-conc1-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc1-rep abnf::cst) (cst-expression-conc1-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc2-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 2)))) (let ((__function__ 'cst-expression-conc2-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-expression-conc2 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-expression-conc2-rep (b* ((abnf::csts (cst-expression-conc2-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc2-rep-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 2)) (b* ((abnf::csts (cst-expression-conc2-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "function-call"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc2-rep-of-tree-fix-cst (equal (cst-expression-conc2-rep (abnf::tree-fix abnf::cst)) (cst-expression-conc2-rep abnf::cst)))
Theorem:
(defthm cst-expression-conc2-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc2-rep abnf::cst) (cst-expression-conc2-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc3-rep (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 3)))) (let ((__function__ 'cst-expression-conc3-rep)) (declare (ignorable __function__)) (abnf::tree-list-fix (nth 0 (cst-expression-conc3 abnf::cst)))))
Theorem:
(defthm tree-listp-of-cst-expression-conc3-rep (b* ((abnf::csts (cst-expression-conc3-rep abnf::cst))) (abnf::tree-listp abnf::csts)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc3-rep-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 3)) (b* ((abnf::csts (cst-expression-conc3-rep abnf::cst))) (cst-list-rep-matchp abnf::csts "literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc3-rep-of-tree-fix-cst (equal (cst-expression-conc3-rep (abnf::tree-fix abnf::cst)) (cst-expression-conc3-rep abnf::cst)))
Theorem:
(defthm cst-expression-conc3-rep-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc3-rep abnf::cst) (cst-expression-conc3-rep cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-dquote-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "dquote"))) (let ((__function__ 'cst-dquote-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-dquote-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-dquote-conc-rep-elem (b* ((abnf::cst1 (cst-dquote-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-dquote-conc-rep-elem-match (implies (cst-matchp abnf::cst "dquote") (b* ((abnf::cst1 (cst-dquote-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x22"))) :rule-classes :rewrite)
Theorem:
(defthm cst-dquote-conc-rep-elem-of-tree-fix-cst (equal (cst-dquote-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-dquote-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-dquote-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-dquote-conc-rep-elem abnf::cst) (cst-dquote-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-squote-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "squote"))) (let ((__function__ 'cst-squote-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-squote-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-squote-conc-rep-elem (b* ((abnf::cst1 (cst-squote-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-squote-conc-rep-elem-match (implies (cst-matchp abnf::cst "squote") (b* ((abnf::cst1 (cst-squote-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x27"))) :rule-classes :rewrite)
Theorem:
(defthm cst-squote-conc-rep-elem-of-tree-fix-cst (equal (cst-squote-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-squote-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-squote-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-squote-conc-rep-elem abnf::cst) (cst-squote-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lf-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lf"))) (let ((__function__ 'cst-lf-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-lf-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-lf-conc-rep-elem (b* ((abnf::cst1 (cst-lf-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-lf-conc-rep-elem-match (implies (cst-matchp abnf::cst "lf") (b* ((abnf::cst1 (cst-lf-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%xA"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lf-conc-rep-elem-of-tree-fix-cst (equal (cst-lf-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-lf-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-lf-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lf-conc-rep-elem abnf::cst) (cst-lf-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-cr-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "cr"))) (let ((__function__ 'cst-cr-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-cr-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-cr-conc-rep-elem (b* ((abnf::cst1 (cst-cr-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-cr-conc-rep-elem-match (implies (cst-matchp abnf::cst "cr") (b* ((abnf::cst1 (cst-cr-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%xD"))) :rule-classes :rewrite)
Theorem:
(defthm cst-cr-conc-rep-elem-of-tree-fix-cst (equal (cst-cr-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-cr-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-cr-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-cr-conc-rep-elem abnf::cst) (cst-cr-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-decimal-digit-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "decimal-digit"))) (let ((__function__ 'cst-decimal-digit-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-decimal-digit-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-decimal-digit-conc-rep-elem (b* ((abnf::cst1 (cst-decimal-digit-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-digit-conc-rep-elem-match (implies (cst-matchp abnf::cst "decimal-digit") (b* ((abnf::cst1 (cst-decimal-digit-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x30-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-decimal-digit-conc-rep-elem-of-tree-fix-cst (equal (cst-decimal-digit-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-decimal-digit-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-decimal-digit-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-decimal-digit-conc-rep-elem abnf::cst) (cst-decimal-digit-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-nonzero-decimal-digit-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "nonzero-decimal-digit"))) (let ((__function__ 'cst-nonzero-decimal-digit-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-nonzero-decimal-digit-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-nonzero-decimal-digit-conc-rep-elem (b* ((abnf::cst1 (cst-nonzero-decimal-digit-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-nonzero-decimal-digit-conc-rep-elem-match (implies (cst-matchp abnf::cst "nonzero-decimal-digit") (b* ((abnf::cst1 (cst-nonzero-decimal-digit-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x31-39"))) :rule-classes :rewrite)
Theorem:
(defthm cst-nonzero-decimal-digit-conc-rep-elem-of-tree-fix-cst (equal (cst-nonzero-decimal-digit-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-nonzero-decimal-digit-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-nonzero-decimal-digit-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-nonzero-decimal-digit-conc-rep-elem abnf::cst) (cst-nonzero-decimal-digit-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 1)))) (let ((__function__ 'cst-literal-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-literal-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-literal-conc1-rep-elem (b* ((abnf::cst1 (cst-literal-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-literal-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "decimal-number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc1-rep-elem-of-tree-fix-cst (equal (cst-literal-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-literal-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-literal-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc1-rep-elem abnf::cst) (cst-literal-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 2)))) (let ((__function__ 'cst-literal-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-literal-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-literal-conc2-rep-elem (b* ((abnf::cst1 (cst-literal-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-literal-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "hex-number"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc2-rep-elem-of-tree-fix-cst (equal (cst-literal-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-literal-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-literal-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc2-rep-elem abnf::cst) (cst-literal-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc3-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 3)))) (let ((__function__ 'cst-literal-conc3-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-literal-conc3-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-literal-conc3-rep-elem (b* ((abnf::cst1 (cst-literal-conc3-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc3-rep-elem-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 3)) (b* ((abnf::cst1 (cst-literal-conc3-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "boolean"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc3-rep-elem-of-tree-fix-cst (equal (cst-literal-conc3-rep-elem (abnf::tree-fix abnf::cst)) (cst-literal-conc3-rep-elem abnf::cst)))
Theorem:
(defthm cst-literal-conc3-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc3-rep-elem abnf::cst) (cst-literal-conc3-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc4-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 4)))) (let ((__function__ 'cst-literal-conc4-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-literal-conc4-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-literal-conc4-rep-elem (b* ((abnf::cst1 (cst-literal-conc4-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc4-rep-elem-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 4)) (b* ((abnf::cst1 (cst-literal-conc4-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "string-literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc4-rep-elem-of-tree-fix-cst (equal (cst-literal-conc4-rep-elem (abnf::tree-fix abnf::cst)) (cst-literal-conc4-rep-elem abnf::cst)))
Theorem:
(defthm cst-literal-conc4-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc4-rep-elem abnf::cst) (cst-literal-conc4-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-literal-conc5-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 5)))) (let ((__function__ 'cst-literal-conc5-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-literal-conc5-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-literal-conc5-rep-elem (b* ((abnf::cst1 (cst-literal-conc5-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc5-rep-elem-match (implies (and (cst-matchp abnf::cst "literal") (equal (cst-literal-conc? abnf::cst) 5)) (b* ((abnf::cst1 (cst-literal-conc5-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "hex-string"))) :rule-classes :rewrite)
Theorem:
(defthm cst-literal-conc5-rep-elem-of-tree-fix-cst (equal (cst-literal-conc5-rep-elem (abnf::tree-fix abnf::cst)) (cst-literal-conc5-rep-elem abnf::cst)))
Theorem:
(defthm cst-literal-conc5-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-literal-conc5-rep-elem abnf::cst) (cst-literal-conc5-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lowercase-letter-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "lowercase-letter"))) (let ((__function__ 'cst-lowercase-letter-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-lowercase-letter-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-lowercase-letter-conc-rep-elem (b* ((abnf::cst1 (cst-lowercase-letter-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-rep-elem-match (implies (cst-matchp abnf::cst "lowercase-letter") (b* ((abnf::cst1 (cst-lowercase-letter-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x61-7A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lowercase-letter-conc-rep-elem-of-tree-fix-cst (equal (cst-lowercase-letter-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-lowercase-letter-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-lowercase-letter-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lowercase-letter-conc-rep-elem abnf::cst) (cst-lowercase-letter-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-uppercase-letter-conc-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "uppercase-letter"))) (let ((__function__ 'cst-uppercase-letter-conc-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-uppercase-letter-conc-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-uppercase-letter-conc-rep-elem (b* ((abnf::cst1 (cst-uppercase-letter-conc-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-rep-elem-match (implies (cst-matchp abnf::cst "uppercase-letter") (b* ((abnf::cst1 (cst-uppercase-letter-conc-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "%x41-5A"))) :rule-classes :rewrite)
Theorem:
(defthm cst-uppercase-letter-conc-rep-elem-of-tree-fix-cst (equal (cst-uppercase-letter-conc-rep-elem (abnf::tree-fix abnf::cst)) (cst-uppercase-letter-conc-rep-elem abnf::cst)))
Theorem:
(defthm cst-uppercase-letter-conc-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-uppercase-letter-conc-rep-elem abnf::cst) (cst-uppercase-letter-conc-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-identifier-rest-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 1)))) (let ((__function__ 'cst-identifier-rest-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-identifier-rest-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-identifier-rest-conc1-rep-elem (b* ((abnf::cst1 (cst-identifier-rest-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-identifier-rest-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "identifier-start"))) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc1-rep-elem-of-tree-fix-cst (equal (cst-identifier-rest-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-identifier-rest-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-identifier-rest-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-rest-conc1-rep-elem abnf::cst) (cst-identifier-rest-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-identifier-rest-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 2)))) (let ((__function__ 'cst-identifier-rest-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-identifier-rest-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-identifier-rest-conc2-rep-elem (b* ((abnf::cst1 (cst-identifier-rest-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "identifier-rest") (equal (cst-identifier-rest-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-identifier-rest-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "decimal-digit"))) :rule-classes :rewrite)
Theorem:
(defthm cst-identifier-rest-conc2-rep-elem-of-tree-fix-cst (equal (cst-identifier-rest-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-identifier-rest-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-identifier-rest-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-identifier-rest-conc2-rep-elem abnf::cst) (cst-identifier-rest-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-comment-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 1)))) (let ((__function__ 'cst-comment-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-comment-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-comment-conc1-rep-elem (b* ((abnf::cst1 (cst-comment-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-comment-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "block-comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc1-rep-elem-of-tree-fix-cst (equal (cst-comment-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-comment-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-comment-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-comment-conc1-rep-elem abnf::cst) (cst-comment-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-comment-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 2)))) (let ((__function__ 'cst-comment-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-comment-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-comment-conc2-rep-elem (b* ((abnf::cst1 (cst-comment-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "comment") (equal (cst-comment-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-comment-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "end-of-line-comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-comment-conc2-rep-elem-of-tree-fix-cst (equal (cst-comment-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-comment-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-comment-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-comment-conc2-rep-elem abnf::cst) (cst-comment-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)))) (let ((__function__ 'cst-token-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-token-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-token-conc1-rep-elem (b* ((abnf::cst1 (cst-token-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-token-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "keyword"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc1-rep-elem-of-tree-fix-cst (equal (cst-token-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-token-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-token-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc1-rep-elem abnf::cst) (cst-token-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)))) (let ((__function__ 'cst-token-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-token-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-token-conc2-rep-elem (b* ((abnf::cst1 (cst-token-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-token-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc2-rep-elem-of-tree-fix-cst (equal (cst-token-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-token-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-token-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc2-rep-elem abnf::cst) (cst-token-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc3-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)))) (let ((__function__ 'cst-token-conc3-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-token-conc3-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-token-conc3-rep-elem (b* ((abnf::cst1 (cst-token-conc3-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-rep-elem-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 3)) (b* ((abnf::cst1 (cst-token-conc3-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "identifier"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc3-rep-elem-of-tree-fix-cst (equal (cst-token-conc3-rep-elem (abnf::tree-fix abnf::cst)) (cst-token-conc3-rep-elem abnf::cst)))
Theorem:
(defthm cst-token-conc3-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc3-rep-elem abnf::cst) (cst-token-conc3-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-token-conc4-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)))) (let ((__function__ 'cst-token-conc4-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-token-conc4-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-token-conc4-rep-elem (b* ((abnf::cst1 (cst-token-conc4-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-rep-elem-match (implies (and (cst-matchp abnf::cst "token") (equal (cst-token-conc? abnf::cst) 4)) (b* ((abnf::cst1 (cst-token-conc4-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "symbol"))) :rule-classes :rewrite)
Theorem:
(defthm cst-token-conc4-rep-elem-of-tree-fix-cst (equal (cst-token-conc4-rep-elem (abnf::tree-fix abnf::cst)) (cst-token-conc4-rep-elem abnf::cst)))
Theorem:
(defthm cst-token-conc4-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-token-conc4-rep-elem abnf::cst) (cst-token-conc4-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)))) (let ((__function__ 'cst-lexeme-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-lexeme-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-lexeme-conc1-rep-elem (b* ((abnf::cst1 (cst-lexeme-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-lexeme-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "token"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc1-rep-elem-of-tree-fix-cst (equal (cst-lexeme-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-lexeme-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-lexeme-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc1-rep-elem abnf::cst) (cst-lexeme-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)))) (let ((__function__ 'cst-lexeme-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-lexeme-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-lexeme-conc2-rep-elem (b* ((abnf::cst1 (cst-lexeme-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-lexeme-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "comment"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc2-rep-elem-of-tree-fix-cst (equal (cst-lexeme-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-lexeme-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-lexeme-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc2-rep-elem abnf::cst) (cst-lexeme-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-lexeme-conc3-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 3)))) (let ((__function__ 'cst-lexeme-conc3-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-lexeme-conc3-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-lexeme-conc3-rep-elem (b* ((abnf::cst1 (cst-lexeme-conc3-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc3-rep-elem-match (implies (and (cst-matchp abnf::cst "lexeme") (equal (cst-lexeme-conc? abnf::cst) 3)) (b* ((abnf::cst1 (cst-lexeme-conc3-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "whitespace"))) :rule-classes :rewrite)
Theorem:
(defthm cst-lexeme-conc3-rep-elem-of-tree-fix-cst (equal (cst-lexeme-conc3-rep-elem (abnf::tree-fix abnf::cst)) (cst-lexeme-conc3-rep-elem abnf::cst)))
Theorem:
(defthm cst-lexeme-conc3-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-lexeme-conc3-rep-elem abnf::cst) (cst-lexeme-conc3-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc1-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 1)))) (let ((__function__ 'cst-expression-conc1-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-expression-conc1-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-expression-conc1-rep-elem (b* ((abnf::cst1 (cst-expression-conc1-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc1-rep-elem-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 1)) (b* ((abnf::cst1 (cst-expression-conc1-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "path"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc1-rep-elem-of-tree-fix-cst (equal (cst-expression-conc1-rep-elem (abnf::tree-fix abnf::cst)) (cst-expression-conc1-rep-elem abnf::cst)))
Theorem:
(defthm cst-expression-conc1-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc1-rep-elem abnf::cst) (cst-expression-conc1-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc2-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 2)))) (let ((__function__ 'cst-expression-conc2-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-expression-conc2-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-expression-conc2-rep-elem (b* ((abnf::cst1 (cst-expression-conc2-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc2-rep-elem-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 2)) (b* ((abnf::cst1 (cst-expression-conc2-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "function-call"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc2-rep-elem-of-tree-fix-cst (equal (cst-expression-conc2-rep-elem (abnf::tree-fix abnf::cst)) (cst-expression-conc2-rep-elem abnf::cst)))
Theorem:
(defthm cst-expression-conc2-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc2-rep-elem abnf::cst) (cst-expression-conc2-rep-elem cst-equiv))) :rule-classes :congruence)
Function:
(defun cst-expression-conc3-rep-elem (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 3)))) (let ((__function__ 'cst-expression-conc3-rep-elem)) (declare (ignorable __function__)) (abnf::tree-fix (nth 0 (cst-expression-conc3-rep abnf::cst)))))
Theorem:
(defthm treep-of-cst-expression-conc3-rep-elem (b* ((abnf::cst1 (cst-expression-conc3-rep-elem abnf::cst))) (abnf::treep abnf::cst1)) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc3-rep-elem-match (implies (and (cst-matchp abnf::cst "expression") (equal (cst-expression-conc? abnf::cst) 3)) (b* ((abnf::cst1 (cst-expression-conc3-rep-elem abnf::cst))) (cst-matchp abnf::cst1 "literal"))) :rule-classes :rewrite)
Theorem:
(defthm cst-expression-conc3-rep-elem-of-tree-fix-cst (equal (cst-expression-conc3-rep-elem (abnf::tree-fix abnf::cst)) (cst-expression-conc3-rep-elem abnf::cst)))
Theorem:
(defthm cst-expression-conc3-rep-elem-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-expression-conc3-rep-elem abnf::cst) (cst-expression-conc3-rep-elem cst-equiv))) :rule-classes :congruence)