Function:
(defun pdf-cst-dict-value-conc? (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (pdf-cst-matchp cst "dict-value"))) (let ((__function__ 'pdf-cst-dict-value-conc?)) (declare (ignorable __function__)) (cond ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "boolean")) 1) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "number")) 2) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "name")) 3) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "array")) 4) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "dictionary")) 5) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "null")) 6) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "rectangle")) 7) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "reference")) 8) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "string")) 9) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-pdf-cst-dict-value-conc? (b* ((number (pdf-cst-dict-value-conc? cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm pdf-cst-dict-value-conc?-possibilities (b* ((number (pdf-cst-dict-value-conc? cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4) (equal number 5) (equal number 6) (equal number 7) (equal number 8) (equal number 9))) :rule-classes ((:forward-chaining :trigger-terms ((pdf-cst-dict-value-conc? cst)))))
Theorem:
(defthm pdf-cst-dict-value-conc?-of-tree-fix-cst (equal (pdf-cst-dict-value-conc? (tree-fix cst)) (pdf-cst-dict-value-conc? cst)))
Theorem:
(defthm pdf-cst-dict-value-conc?-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (pdf-cst-dict-value-conc? cst) (pdf-cst-dict-value-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm pdf-cst-dict-value-conc?-1-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 1) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "boolean"))))
Theorem:
(defthm pdf-cst-dict-value-conc?-2-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 2) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "number"))))
Theorem:
(defthm pdf-cst-dict-value-conc?-3-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 3) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "name"))))
Theorem:
(defthm pdf-cst-dict-value-conc?-4-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 4) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "array"))))
Theorem:
(defthm pdf-cst-dict-value-conc?-5-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 5) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "dictionary"))))
Theorem:
(defthm pdf-cst-dict-value-conc?-6-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 6) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "null"))))
Theorem:
(defthm pdf-cst-dict-value-conc?-7-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 7) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "rectangle"))))
Theorem:
(defthm pdf-cst-dict-value-conc?-8-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 8) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "reference"))))
Theorem:
(defthm pdf-cst-dict-value-conc?-9-iff-match-conc (implies (pdf-cst-matchp cst "dict-value") (iff (equal (pdf-cst-dict-value-conc? cst) 9) (pdf-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "string"))))