Generate the formula of the theorem that says that the new function maps values in the new representation to values in the old representation.
(isodata-gen-newp-of-new-thm-formula old$ arg-isomaps res-isomaps new$ wrld) → formula
Function:
(defun isodata-gen-newp-of-new-thm-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)))) (declare (xargs :guard (consp res-isomaps))) (let ((__function__ 'isodata-gen-newp-of-new-thm-formula)) (declare (ignorable __function__)) (b* ((x1...xn (formals old$ wrld)) (newp-of-x1...xn (isodata-gen-newp-of-terms x1...xn arg-isomaps)) (newp-of-x1...xn-conj (conjoin newp-of-x1...xn)) (new-call (fcons-term new$ x1...xn)) (m (len res-isomaps))) (if (= m 1) (b* ((res-isomap (cdar res-isomaps)) (newp-res (isodata-isomap->newp res-isomap))) (implicate newp-of-x1...xn-conj (fcons-term* newp-res new-call))) (b* ((y1...ym (isodata-gen-result-vars new$ m)) (newp-of-y1...ym (isodata-gen-newp-of-terms y1...ym res-isomaps))) (implicate newp-of-x1...xn-conj (make-mv-let-call 'mv y1...ym :all new-call (conjoin newp-of-y1...ym))))))))