		Search-engine friendly clone of the ACL2 documentation.

Grammar

Cst-list-rep-matchp$

Signature
(cst-list-rep-matchp$ abnf::trees abnf::rep) → abnf::yes/no
Arguments: abnf::trees — Guard (abnf::tree-listp abnf::trees).; abnf::rep — Guard (abnf::repetitionp abnf::rep).
Returns: abnf::yes/no — Type (booleanp abnf::yes/no).

Definitions and Theorems

Function: cst-list-rep-matchp$

(defun cst-list-rep-matchp$ (abnf::trees abnf::rep)
  (declare (xargs :guard (and (abnf::tree-listp abnf::trees)
                              (abnf::repetitionp abnf::rep))))
  (let ((__function__ 'cst-list-rep-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-list-terminatedp abnf::trees)
         (abnf::tree-list-match-repetition-p
              abnf::trees abnf::rep *grammar*))))

Theorem: booleanp-of-cst-list-rep-matchp$

(defthm booleanp-of-cst-list-rep-matchp$
  (b* ((abnf::yes/no (cst-list-rep-matchp$ abnf::trees abnf::rep)))
    (booleanp abnf::yes/no))
  :rule-classes :rewrite)

Theorem: cst-list-rep-matchp$-of-tree-list-fix-trees

(defthm cst-list-rep-matchp$-of-tree-list-fix-trees
  (equal (cst-list-rep-matchp$ (abnf::tree-list-fix abnf::trees)
                               abnf::rep)
         (cst-list-rep-matchp$ abnf::trees abnf::rep)))

Theorem: cst-list-rep-matchp$-tree-list-equiv-congruence-on-trees

(defthm cst-list-rep-matchp$-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv abnf::trees trees-equiv)
           (equal (cst-list-rep-matchp$ abnf::trees abnf::rep)
                  (cst-list-rep-matchp$ trees-equiv abnf::rep)))
  :rule-classes :congruence)

Theorem: cst-list-rep-matchp$-of-repetition-fix-rep

(defthm cst-list-rep-matchp$-of-repetition-fix-rep
  (equal (cst-list-rep-matchp$ abnf::trees
                               (abnf::repetition-fix abnf::rep))
         (cst-list-rep-matchp$ abnf::trees abnf::rep)))

Theorem: cst-list-rep-matchp$-repetition-equiv-congruence-on-rep

(defthm cst-list-rep-matchp$-repetition-equiv-congruence-on-rep
  (implies (abnf::repetition-equiv abnf::rep rep-equiv)
           (equal (cst-list-rep-matchp$ abnf::trees abnf::rep)
                  (cst-list-rep-matchp$ abnf::trees rep-equiv)))
  :rule-classes :congruence)