(cst-statement-expression-conc? abnf::cst) → number
Function:
(defun cst-statement-expression-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "statement-expression"))) (let ((__function__ 'cst-statement-expression-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "assignment")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "pre-increment-expression")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "pre-decrement-expression")) 3) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "post-increment-expression")) 4) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "post-decrement-expression")) 5) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "method-invocation")) 6) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "class-instance-creation-expression")) 7) (t (prog2$ (impossible) 1)))))
Theorem:
(defthm posp-of-cst-statement-expression-conc? (b* ((number (cst-statement-expression-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-statement-expression-conc?-possibilities (b* ((number (cst-statement-expression-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4) (equal number 5) (equal number 6) (equal number 7))) :rule-classes ((:forward-chaining :trigger-terms ((cst-statement-expression-conc? abnf::cst)))))
Theorem:
(defthm cst-statement-expression-conc?-of-tree-fix-cst (equal (cst-statement-expression-conc? (abnf::tree-fix abnf::cst)) (cst-statement-expression-conc? abnf::cst)))
Theorem:
(defthm cst-statement-expression-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-statement-expression-conc? abnf::cst) (cst-statement-expression-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-statement-expression-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "statement-expression") (iff (equal (cst-statement-expression-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "assignment"))))
Theorem:
(defthm cst-statement-expression-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "statement-expression") (iff (equal (cst-statement-expression-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "pre-increment-expression"))))
Theorem:
(defthm cst-statement-expression-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "statement-expression") (iff (equal (cst-statement-expression-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "pre-decrement-expression"))))
Theorem:
(defthm cst-statement-expression-conc?-4-iff-match-conc (implies (cst-matchp abnf::cst "statement-expression") (iff (equal (cst-statement-expression-conc? abnf::cst) 4) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "post-increment-expression"))))
Theorem:
(defthm cst-statement-expression-conc?-5-iff-match-conc (implies (cst-matchp abnf::cst "statement-expression") (iff (equal (cst-statement-expression-conc? abnf::cst) 5) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "post-decrement-expression"))))
Theorem:
(defthm cst-statement-expression-conc?-6-iff-match-conc (implies (cst-matchp abnf::cst "statement-expression") (iff (equal (cst-statement-expression-conc? abnf::cst) 6) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "method-invocation"))))
Theorem:
(defthm cst-statement-expression-conc?-7-iff-match-conc (implies (cst-matchp abnf::cst "statement-expression") (iff (equal (cst-statement-expression-conc? abnf::cst) 7) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "class-instance-creation-expression"))))