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