Generate the hints to prove the theorem that relates the old and new function, when the result of a single-valued function is being transformed.
(expdata-gen-old-to-new-thm-hints-1res appcond-thm-names old$ arg-surjmaps res-surjmaps new-to-old$ wrld) → hints
Function:
(defun expdata-gen-old-to-new-thm-hints-1res (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-1res)) (declare (ignorable __function__)) (b* ((oldp-of-old (cdr (assoc-eq :oldp-of-old appcond-thm-names))) (instances-forth-image (expdata-gen-forth-image-instances-to-x1...xn arg-surjmaps wrld)) (instances-back-of-forth (expdata-gen-back-of-forth-instances-to-x1...xn arg-surjmaps wrld)) (instance-new-to-old (expdata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn new-to-old$ old$ arg-surjmaps wrld)) (res-surjmap (cdar res-surjmaps)) (back-of-forth-res (expdata-surjmap->back-of-forth res-surjmap)) (var (expdata-formal-of-forth res-surjmap wrld)) (x1...xn (formals old$ wrld)) (old-call (fcons-term old$ x1...xn)) (instance-back-of-forth-res (cons ':instance (cons back-of-forth-res (cons ':extra-bindings-ok (cons (cons var (cons old-call 'nil)) 'nil)))))) (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (append instances-forth-image (append instances-back-of-forth (cons instance-new-to-old (cons oldp-of-old (cons instance-back-of-forth-res 'nil))))) 'nil))))) 'nil))))