		Search-engine friendly clone of the ACL2 documentation.

Grammar

Cst-list-elem-matchp$

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

Definitions and Theorems

Function: cst-list-elem-matchp$

(defun cst-list-elem-matchp$ (abnf::trees abnf::elem)
  (declare (xargs :guard (and (abnf::tree-listp abnf::trees)
                              (abnf::elementp abnf::elem))))
  (let ((__function__ 'cst-list-elem-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-list-terminatedp abnf::trees)
         (abnf::tree-list-match-element-p
              abnf::trees
              abnf::elem *all-grammar-rules*))))

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

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

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

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

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

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

Theorem: cst-list-elem-matchp$-of-element-fix-elem

(defthm cst-list-elem-matchp$-of-element-fix-elem
  (equal (cst-list-elem-matchp$ abnf::trees
                                (abnf::element-fix abnf::elem))
         (cst-list-elem-matchp$ abnf::trees abnf::elem)))

Theorem: cst-list-elem-matchp$-element-equiv-congruence-on-elem

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