Generate the formula of
the lemma use to prove
(isodata-gen-new-to-old-lemma-formula old$ arg-isomaps res-isomaps new$ wrld) → new-to-old-lemma-formula
See isodata-gen-new-to-old-lemma for details.
Function:
(defun isodata-gen-new-to-old-lemma-formula (old$ arg-isomaps res-isomaps new$ wrld) (declare (xargs :guard (and (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (symbolp new$) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-new-to-old-lemma-formula)) (declare (ignorable __function__)) (b* ((x1...xn (formals old$ wrld)) (newp-of-x1...xn (isodata-gen-newp-of-terms x1...xn arg-isomaps)) (back-of-x1...xn (isodata-gen-back-of-terms x1...xn arg-isomaps)) (old-call (fcons-term old$ back-of-x1...xn)) (new-call (fcons-term new$ x1...xn)) (mv-nths-of-new-call (make-mv-nth-calls new-call (len res-isomaps))) (mv-nths-of-old-call (make-mv-nth-calls old-call (len res-isomaps))) (forth-of-mv-nths-of-old-call (isodata-gen-forth-of-terms mv-nths-of-old-call res-isomaps)) (consequent (conjoin-equalities mv-nths-of-new-call forth-of-mv-nths-of-old-call))) (implicate (conjoin newp-of-x1...xn) consequent))))