		Search-engine friendly clone of the ACL2 documentation.

Pdf-example

Pdf-cst-dict-value-conc?

Signature
(pdf-cst-dict-value-conc? cst) → number
Arguments: cst — Guard (treep cst).
Returns: number — Type (posp number).

Definitions and Theorems

Function: pdf-cst-dict-value-conc?

(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: posp-of-pdf-cst-dict-value-conc?

(defthm posp-of-pdf-cst-dict-value-conc?
  (b* ((number (pdf-cst-dict-value-conc? cst)))
    (posp number))
  :rule-classes :rewrite)

Theorem: pdf-cst-dict-value-conc?-possibilities

(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: pdf-cst-dict-value-conc?-of-tree-fix-cst

(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: pdf-cst-dict-value-conc?-tree-equiv-congruence-on-cst

(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: pdf-cst-dict-value-conc?-1-iff-match-conc

(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: pdf-cst-dict-value-conc?-2-iff-match-conc

(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: pdf-cst-dict-value-conc?-3-iff-match-conc

(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: pdf-cst-dict-value-conc?-4-iff-match-conc

(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: pdf-cst-dict-value-conc?-5-iff-match-conc

(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: pdf-cst-dict-value-conc?-6-iff-match-conc

(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: pdf-cst-dict-value-conc?-7-iff-match-conc

(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: pdf-cst-dict-value-conc?-8-iff-match-conc

(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: pdf-cst-dict-value-conc?-9-iff-match-conc

(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"))))