(cst-block-statement-conc? abnf::cst) → number
Function:
(defun cst-block-statement-conc? (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "block-statement"))) (let ((__function__ 'cst-block-statement-conc?)) (declare (ignorable __function__)) (cond ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "local-variable-declaration-statement")) 1) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "class-declaration")) 2) ((equal (abnf::tree-nonleaf->rulename? (nth 0 (nth 0 (abnf::tree-nonleaf->branches abnf::cst)))) (abnf::rulename "statement")) 3) (t (prog2$ (impossible) 1)))))
Theorem:
(defthm posp-of-cst-block-statement-conc? (b* ((number (cst-block-statement-conc? abnf::cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm cst-block-statement-conc?-possibilities (b* ((number (cst-block-statement-conc? abnf::cst))) (or (equal number 1) (equal number 2) (equal number 3))) :rule-classes ((:forward-chaining :trigger-terms ((cst-block-statement-conc? abnf::cst)))))
Theorem:
(defthm cst-block-statement-conc?-of-tree-fix-cst (equal (cst-block-statement-conc? (abnf::tree-fix abnf::cst)) (cst-block-statement-conc? abnf::cst)))
Theorem:
(defthm cst-block-statement-conc?-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-block-statement-conc? abnf::cst) (cst-block-statement-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm cst-block-statement-conc?-1-iff-match-conc (implies (cst-matchp abnf::cst "block-statement") (iff (equal (cst-block-statement-conc? abnf::cst) 1) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "local-variable-declaration-statement"))))
Theorem:
(defthm cst-block-statement-conc?-2-iff-match-conc (implies (cst-matchp abnf::cst "block-statement") (iff (equal (cst-block-statement-conc? abnf::cst) 2) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "class-declaration"))))
Theorem:
(defthm cst-block-statement-conc?-3-iff-match-conc (implies (cst-matchp abnf::cst "block-statement") (iff (equal (cst-block-statement-conc? abnf::cst) 3) (cst-list-list-conc-matchp (abnf::tree-nonleaf->branches abnf::cst) "statement"))))