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