Function:
(defun imf-cst-received-token-conc? (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (imf-cst-matchp cst "received-token"))) (let ((__function__ 'imf-cst-received-token-conc?)) (declare (ignorable __function__)) (cond ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "word")) 1) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "angle-addr")) 2) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "addr-spec")) 3) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "domain")) 4) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-imf-cst-received-token-conc? (b* ((number (imf-cst-received-token-conc? cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm imf-cst-received-token-conc?-possibilities (b* ((number (imf-cst-received-token-conc? cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4))) :rule-classes ((:forward-chaining :trigger-terms ((imf-cst-received-token-conc? cst)))))
Theorem:
(defthm imf-cst-received-token-conc?-of-tree-fix-cst (equal (imf-cst-received-token-conc? (tree-fix cst)) (imf-cst-received-token-conc? cst)))
Theorem:
(defthm imf-cst-received-token-conc?-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (imf-cst-received-token-conc? cst) (imf-cst-received-token-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm imf-cst-received-token-conc?-1-iff-match-conc (implies (imf-cst-matchp cst "received-token") (iff (equal (imf-cst-received-token-conc? cst) 1) (imf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "word"))))
Theorem:
(defthm imf-cst-received-token-conc?-2-iff-match-conc (implies (imf-cst-matchp cst "received-token") (iff (equal (imf-cst-received-token-conc? cst) 2) (imf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "angle-addr"))))
Theorem:
(defthm imf-cst-received-token-conc?-3-iff-match-conc (implies (imf-cst-matchp cst "received-token") (iff (equal (imf-cst-received-token-conc? cst) 3) (imf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "addr-spec"))))
Theorem:
(defthm imf-cst-received-token-conc?-4-iff-match-conc (implies (imf-cst-matchp cst "received-token") (iff (equal (imf-cst-received-token-conc? cst) 4) (imf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "domain"))))