(collect-bfr-eval-vals term patterns) → terms
Theorem:
(defthm return-type-of-collect-bfr-eval-vals.terms (implies (pseudo-termp term) (b* ((?terms (collect-bfr-eval-vals term patterns))) (pseudo-term-listp terms))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-collect-bfr-eval-vals-list.terms (implies (pseudo-term-listp clause) (b* ((?terms (collect-bfr-eval-vals-list clause patterns))) (pseudo-term-listp terms))) :rule-classes :rewrite)