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