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