(cst-statement-without-trailing-substatement-conc? abnf::cst) → number
Function:
(defun cst-statement-without-trailing-substatement-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "statement-without-trailing-substatement"))) (let ((__function__ 'cst-statement-without-trailing-substatement-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "block")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "empty-statement")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "expression-statement")) 3) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "assert-statement")) 4) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "switch-statement")) 5) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "do-statement")) 6) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "break-statement")) 7) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "continue-statement")) 8) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "return-statement")) 9) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "synchronized-statement")) 10) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "throw-statement")) 11) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "try-statement")) 12) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "yield-statement")) 13) (t (prog2$ (impossible) 1)))))
Theorem:
(defthm posp-of-cst-statement-without-trailing-substatement-conc? (b* ((number (cst-statement-without-trailing-substatement-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-possibilities (b* ((number (cst-statement-without-trailing-substatement-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4) (equal number 5) (equal number 6) (equal number 7) (equal number 8) (equal number 9) (equal number 10) (equal number 11) (equal number 12) (equal number 13))) :rule-classes ((:forward-chaining :trigger-terms ((cst-statement-without-trailing-substatement-conc? abnf::cst)))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-of-tree-fix-cst (equal (cst-statement-without-trailing-substatement-conc? (abnf::tree-fix abnf::cst)) (cst-statement-without-trailing-substatement-conc? abnf::cst)))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) (cst-statement-without-trailing-substatement-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "block"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "empty-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "expression-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-4-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 4) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "assert-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-5-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 5) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "switch-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-6-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 6) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "do-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-7-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 7) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "break-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-8-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 8) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "continue-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-9-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 9) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "return-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-10-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 10) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "synchronized-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-11-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 11) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "throw-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-12-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 12) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "try-statement"))))
Theorem:
(defthm cst-statement-without-trailing-substatement-conc?-13-iff-match-conc (implies (cst-matchp abnf::cst "statement-without-trailing-substatement") (iff (equal (cst-statement-without-trailing-substatement-conc? abnf::cst) 13) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "yield-statement"))))