		Search-engine friendly clone of the ACL2 documentation.

Grammar

Cst-list-list-alt-matchp$

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

Definitions and Theorems

Function: cst-list-list-alt-matchp$

(defun cst-list-list-alt-matchp$ (abnf::treess abnf::alt)
  (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess)
                              (abnf::alternationp abnf::alt))))
  (let ((__function__ 'cst-list-list-alt-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-list-list-terminatedp abnf::treess)
         (abnf::tree-list-list-match-alternation-p
              abnf::treess abnf::alt *grammar*))))

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

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

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

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

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

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

Theorem: cst-list-list-alt-matchp$-of-alternation-fix-alt

(defthm cst-list-list-alt-matchp$-of-alternation-fix-alt
  (equal
       (cst-list-list-alt-matchp$ abnf::treess
                                  (abnf::alternation-fix abnf::alt))
       (cst-list-list-alt-matchp$ abnf::treess abnf::alt)))

Theorem: cst-list-list-alt-matchp$-alternation-equiv-congruence-on-alt

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