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