Restore and calls in a translated term.
(atj-restore-and-calls-in-term term) → new-term
Recall that, at this point, terms have already been type-annotated. Thus, we must take the type annotations into account here, as we recognize and transform the terms.
Theorem:
(defthm return-type-of-atj-restore-and-calls-in-term.new-term (b* ((?new-term (atj-restore-and-calls-in-term term))) (pseudo-termp new-term)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-restore-and-calls-in-terms.new-terms (b* ((?new-terms (atj-restore-and-calls-in-terms terms))) (pseudo-term-listp new-terms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-restore-and-calls-in-terms (b* ((?new-terms (atj-restore-and-calls-in-terms terms))) (equal (len new-terms) (len terms))))