		Search-engine friendly clone of the ACL2 documentation.

Grammar

Cst-list-list-conc-matchp$

Signature
(cst-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: cst-list-list-conc-matchp$

(defun cst-list-list-conc-matchp$ (abnf::treess abnf::conc)
  (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess)
                              (abnf::concatenationp abnf::conc))))
  (let ((__function__ 'cst-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*))))

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

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

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

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

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

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

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

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

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

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