Generate the hints to prove the theorem that expresses the new function in terms of the old function.
(isodata-gen-new-to-old-thm-hints appcond-thm-names old$ arg-isomaps res-isomaps new$ old-fn-unnorm-name new-fn-unnorm-name new-to-old-lemma-name new-to-list-of-mv-nth-name wrld) → hints
Function:
(defun isodata-gen-new-to-old-thm-hints (appcond-thm-names old$ arg-isomaps res-isomaps new$ old-fn-unnorm-name new-fn-unnorm-name new-to-old-lemma-name new-to-list-of-mv-nth-name wrld) (declare (xargs :guard (and (symbol-symbol-alistp appcond-thm-names) (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (symbolp new$) (symbolp old-fn-unnorm-name) (symbolp new-fn-unnorm-name) (symbolp new-to-old-lemma-name) (symbolp new-to-list-of-mv-nth-name) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-new-to-old-thm-hints)) (declare (ignorable __function__)) (case (len res-isomaps) (0 (isodata-gen-new-to-old-thm-hints-0res appcond-thm-names old$ arg-isomaps new$ old-fn-unnorm-name new-fn-unnorm-name wrld)) (1 (isodata-gen-new-to-old-thm-hints-1res appcond-thm-names old$ arg-isomaps res-isomaps new$ old-fn-unnorm-name new-fn-unnorm-name wrld)) (t (isodata-gen-new-to-old-thm-hints-mres new-to-old-lemma-name new-to-list-of-mv-nth-name)))))