		Search-engine friendly clone of the ACL2 documentation.

Pdf-example

Pdf-cst-list-list-conc-matchp$

Signature
(pdf-cst-list-list-conc-matchp$ treess conc) → yes/no
Arguments: treess — Guard (tree-list-listp treess).; conc — Guard (concatenationp conc).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: pdf-cst-list-list-conc-matchp$

(defun pdf-cst-list-list-conc-matchp$ (treess conc)
  (declare (xargs :guard (and (tree-list-listp treess)
                              (concatenationp conc))))
  (let ((__function__ 'pdf-cst-list-list-conc-matchp$))
    (declare (ignorable __function__))
    (and (tree-list-list-terminatedp treess)
         (tree-list-list-match-concatenation-p
              treess conc *pdf-grammar-rules*))))

Theorem: booleanp-of-pdf-cst-list-list-conc-matchp$

(defthm booleanp-of-pdf-cst-list-list-conc-matchp$
  (b* ((yes/no (pdf-cst-list-list-conc-matchp$ treess conc)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: pdf-cst-list-list-conc-matchp$-of-tree-list-list-fix-treess

(defthm pdf-cst-list-list-conc-matchp$-of-tree-list-list-fix-treess
  (equal (pdf-cst-list-list-conc-matchp$ (tree-list-list-fix treess)
                                         conc)
         (pdf-cst-list-list-conc-matchp$ treess conc)))

Theorem: pdf-cst-list-list-conc-matchp$-tree-list-list-equiv-congruence-on-treess

(defthm
 pdf-cst-list-list-conc-matchp$-tree-list-list-equiv-congruence-on-treess
 (implies
      (tree-list-list-equiv treess treess-equiv)
      (equal (pdf-cst-list-list-conc-matchp$ treess conc)
             (pdf-cst-list-list-conc-matchp$ treess-equiv conc)))
 :rule-classes :congruence)

Theorem: pdf-cst-list-list-conc-matchp$-of-concatenation-fix-conc

(defthm pdf-cst-list-list-conc-matchp$-of-concatenation-fix-conc
 (equal
    (pdf-cst-list-list-conc-matchp$ treess (concatenation-fix conc))
    (pdf-cst-list-list-conc-matchp$ treess conc)))

Theorem: pdf-cst-list-list-conc-matchp$-concatenation-equiv-congruence-on-conc

(defthm
 pdf-cst-list-list-conc-matchp$-concatenation-equiv-congruence-on-conc
 (implies
      (concatenation-equiv conc conc-equiv)
      (equal (pdf-cst-list-list-conc-matchp$ treess conc)
             (pdf-cst-list-list-conc-matchp$ treess conc-equiv)))
 :rule-classes :congruence)