Generate the formula of the theorem that expresses the new function in terms of the old function.
(expdata-gen-new-to-old-thm-formula old$ arg-surjmaps res-surjmaps new$ wrld) → new-to-old-formula
Function:
(defun expdata-gen-new-to-old-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)))) (let ((__function__ 'expdata-gen-new-to-old-thm-formula)) (declare (ignorable __function__)) (b* ((x1...xn (formals old$ wrld)) (newp-of-x1...xn (expdata-gen-newp-of-terms x1...xn arg-surjmaps)) (back-of-x1...xn (expdata-gen-back-of-terms x1...xn arg-surjmaps)) (old-call (fcons-term old$ back-of-x1...xn)) (new-call (fcons-term new$ x1...xn)) (consequent (case (len res-surjmaps) (0 (cons 'equal (cons new-call (cons old-call 'nil)))) (1 (b* ((forth-res (expdata-surjmap->forth (cdar res-surjmaps))) (forth-of-old-call (apply-term* forth-res old-call))) (cons 'equal (cons new-call (cons forth-of-old-call 'nil))))) (t (b* ((mv-nths-of-new-call (make-mv-nth-calls new-call (len res-surjmaps))) (mv-nths-of-old-call (make-mv-nth-calls old-call (len res-surjmaps))) (forth-of-mv-nths-of-old-call (expdata-gen-forth-of-terms mv-nths-of-old-call res-surjmaps))) (conjoin-equalities mv-nths-of-new-call forth-of-mv-nths-of-old-call)))))) (implicate (conjoin newp-of-x1...xn) consequent))))