Generate the formula of the theorem that says that the new function maps values in the new representation to values in the old representation.
(expdata-gen-newp-of-new-thm-formula old$ arg-surjmaps res-surjmaps new$ wrld) → formula
Function:
(defun expdata-gen-newp-of-new-thm-formula (old$ arg-surjmaps res-surjmaps new$ wrld) (declare (xargs :guard (and (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (expdata-pos-surjmap-alistp res-surjmaps) (symbolp new$) (plist-worldp wrld)))) (declare (xargs :guard (consp res-surjmaps))) (let ((__function__ 'expdata-gen-newp-of-new-thm-formula)) (declare (ignorable __function__)) (b* ((x1...xn (formals old$ wrld)) (newp-of-x1...xn (expdata-gen-newp-of-terms x1...xn arg-surjmaps)) (newp-of-x1...xn-conj (conjoin newp-of-x1...xn)) (new-call (fcons-term new$ x1...xn)) (m (len res-surjmaps))) (if (= m 1) (b* ((res-surjmap (cdar res-surjmaps)) (newp-res (expdata-surjmap->newp res-surjmap))) (implicate newp-of-x1...xn-conj (fcons-term* newp-res new-call))) (b* ((y1...ym (expdata-gen-result-vars new$ m)) (newp-of-y1...ym (expdata-gen-newp-of-terms y1...ym res-surjmaps))) (implicate newp-of-x1...xn-conj (make-mv-let-call 'mv y1...ym :all new-call (conjoin newp-of-y1...ym))))))))