(cst-statement-conc? abnf::cst) → number
Function:
(defun cst-statement-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "statement"))) (let ((__function__ 'cst-statement-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "statement-without-trailing-substatement")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "labeled-statement")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "if-then-statement")) 3) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "if-then-else-statement")) 4) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "while-statement")) 5) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "for-statement")) 6) (t (prog2$ (impossible) 1)))))
Theorem:
(defthm posp-of-cst-statement-conc? (b* ((number (cst-statement-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-statement-conc?-possibilities (b* ((number (cst-statement-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4) (equal number 5) (equal number 6))) :rule-classes ((:forward-chaining :trigger-terms ((cst-statement-conc? abnf::cst)))))
Theorem:
(defthm cst-statement-conc?-of-tree-fix-cst (equal (cst-statement-conc? (abnf::tree-fix abnf::cst)) (cst-statement-conc? abnf::cst)))
Theorem:
(defthm cst-statement-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-statement-conc? abnf::cst) (cst-statement-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-statement-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "statement") (iff (equal (cst-statement-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "statement-without-trailing-substatement"))))
Theorem:
(defthm cst-statement-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "statement") (iff (equal (cst-statement-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "labeled-statement"))))
Theorem:
(defthm cst-statement-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "statement") (iff (equal (cst-statement-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "if-then-statement"))))
Theorem:
(defthm cst-statement-conc?-4-iff-match-conc (implies (cst-matchp abnf::cst "statement") (iff (equal (cst-statement-conc? abnf::cst) 4) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "if-then-else-statement"))))
Theorem:
(defthm cst-statement-conc?-5-iff-match-conc (implies (cst-matchp abnf::cst "statement") (iff (equal (cst-statement-conc? abnf::cst) 5) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "while-statement"))))
Theorem:
(defthm cst-statement-conc?-6-iff-match-conc (implies (cst-matchp abnf::cst "statement") (iff (equal (cst-statement-conc? abnf::cst) 6) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "for-statement"))))