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