Generate the hints to prove the theorem that relates the old and new function, when no result is being transformed.
(isodata-gen-old-to-new-thm-hints-0res old$ arg-isomaps new-to-old$ wrld) → hints
Function:
(defun isodata-gen-old-to-new-thm-hints-0res (old$ arg-isomaps new-to-old$ wrld) (declare (xargs :guard (and (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (symbolp new-to-old$) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-old-to-new-thm-hints-0res)) (declare (ignorable __function__)) (b* ((instances-forth-image (isodata-gen-forth-image-instances-to-x1...xn arg-isomaps wrld)) (instances-back-of-forth (isodata-gen-back-of-forth-instances-to-x1...xn arg-isomaps wrld)) (instance-new-to-old (isodata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn new-to-old$ old$ arg-isomaps wrld))) (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 'nil))) 'nil))))) 'nil))))