		Search-engine friendly clone of the ACL2 documentation.

Grammar-old

Ocst-list-list-conc-matchp$

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

Definitions and Theorems

Function: ocst-list-list-conc-matchp$

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

Theorem: booleanp-of-ocst-list-list-conc-matchp$

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

Theorem: ocst-list-list-conc-matchp$-of-tree-list-list-fix-treess

(defthm ocst-list-list-conc-matchp$-of-tree-list-list-fix-treess
  (equal (ocst-list-list-conc-matchp$
              (abnf::tree-list-list-fix abnf::treess)
              abnf::conc)
         (ocst-list-list-conc-matchp$ abnf::treess abnf::conc)))

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

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

Theorem: ocst-list-list-conc-matchp$-of-concatenation-fix-conc

(defthm ocst-list-list-conc-matchp$-of-concatenation-fix-conc
 (equal
  (ocst-list-list-conc-matchp$ abnf::treess
                               (abnf::concatenation-fix abnf::conc))
  (ocst-list-list-conc-matchp$ abnf::treess abnf::conc)))

Theorem: ocst-list-list-conc-matchp$-concatenation-equiv-congruence-on-conc

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