Generate the hints to prove the theorem that relates the old and new function.
(expdata-gen-old-to-new-thm-hints appcond-thm-names old$ arg-surjmaps res-surjmaps new-to-old$ wrld) → hints
Function:
(defun expdata-gen-old-to-new-thm-hints (appcond-thm-names old$ arg-surjmaps res-surjmaps new-to-old$ wrld) (declare (xargs :guard (and (symbol-symbol-alistp appcond-thm-names) (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (expdata-pos-surjmap-alistp res-surjmaps) (symbolp new-to-old$) (plist-worldp wrld)))) (let ((__function__ 'expdata-gen-old-to-new-thm-hints)) (declare (ignorable __function__)) (case (len res-surjmaps) (0 (expdata-gen-old-to-new-thm-hints-0res old$ arg-surjmaps new-to-old$ wrld)) (1 (expdata-gen-old-to-new-thm-hints-1res appcond-thm-names old$ arg-surjmaps res-surjmaps new-to-old$ wrld)) (t (expdata-gen-old-to-new-thm-hints-mres appcond-thm-names old$ arg-surjmaps res-surjmaps new-to-old$ wrld)))))