(imap-cst-list-list-alt-matchp$ treess alt) → yes/no
Function:
(defun imap-cst-list-list-alt-matchp$ (treess alt) (declare (xargs :guard (and (tree-list-listp treess) (alternationp alt)))) (let ((__function__ 'imap-cst-list-list-alt-matchp$)) (declare (ignorable __function__)) (and (tree-list-list-terminatedp treess) (tree-list-list-match-alternation-p treess alt *all-imap-grammar-rules*))))
Theorem:
(defthm booleanp-of-imap-cst-list-list-alt-matchp$ (b* ((yes/no (imap-cst-list-list-alt-matchp$ treess alt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm imap-cst-list-list-alt-matchp$-of-tree-list-list-fix-treess (equal (imap-cst-list-list-alt-matchp$ (tree-list-list-fix treess) alt) (imap-cst-list-list-alt-matchp$ treess alt)))
Theorem:
(defthm imap-cst-list-list-alt-matchp$-tree-list-list-equiv-congruence-on-treess (implies (tree-list-list-equiv treess treess-equiv) (equal (imap-cst-list-list-alt-matchp$ treess alt) (imap-cst-list-list-alt-matchp$ treess-equiv alt))) :rule-classes :congruence)
Theorem:
(defthm imap-cst-list-list-alt-matchp$-of-alternation-fix-alt (equal (imap-cst-list-list-alt-matchp$ treess (alternation-fix alt)) (imap-cst-list-list-alt-matchp$ treess alt)))
Theorem:
(defthm imap-cst-list-list-alt-matchp$-alternation-equiv-congruence-on-alt (implies (alternation-equiv alt alt-equiv) (equal (imap-cst-list-list-alt-matchp$ treess alt) (imap-cst-list-list-alt-matchp$ treess alt-equiv))) :rule-classes :congruence)