		Search-engine friendly clone of the ACL2 documentation.

Grammar-old

Ocst-matchp$

Signature
(ocst-matchp$ abnf::tree abnf::elem) → abnf::yes/no
Arguments: abnf::tree — Guard (abnf::treep abnf::tree).; abnf::elem — Guard (abnf::elementp abnf::elem).
Returns: abnf::yes/no — Type (booleanp abnf::yes/no).

Definitions and Theorems

Function: ocst-matchp$

(defun ocst-matchp$ (abnf::tree abnf::elem)
  (declare (xargs :guard (and (abnf::treep abnf::tree)
                              (abnf::elementp abnf::elem))))
  (let ((__function__ 'ocst-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-terminatedp abnf::tree)
         (abnf::tree-match-element-p
              abnf::tree abnf::elem *grammar-old*))))

Theorem: booleanp-of-ocst-matchp$

(defthm booleanp-of-ocst-matchp$
  (b* ((abnf::yes/no (ocst-matchp$ abnf::tree abnf::elem)))
    (booleanp abnf::yes/no))
  :rule-classes :rewrite)

Theorem: ocst-matchp$-of-tree-fix-tree

(defthm ocst-matchp$-of-tree-fix-tree
  (equal (ocst-matchp$ (abnf::tree-fix abnf::tree)
                       abnf::elem)
         (ocst-matchp$ abnf::tree abnf::elem)))

Theorem: ocst-matchp$-tree-equiv-congruence-on-tree

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

Theorem: ocst-matchp$-of-element-fix-elem

(defthm ocst-matchp$-of-element-fix-elem
  (equal (ocst-matchp$ abnf::tree
                       (abnf::element-fix abnf::elem))
         (ocst-matchp$ abnf::tree abnf::elem)))

Theorem: ocst-matchp$-element-equiv-congruence-on-elem

(defthm ocst-matchp$-element-equiv-congruence-on-elem
  (implies (abnf::element-equiv abnf::elem elem-equiv)
           (equal (ocst-matchp$ abnf::tree abnf::elem)
                  (ocst-matchp$ abnf::tree elem-equiv)))
  :rule-classes :congruence)