Generate the hints to verify the guards of the new function,
when
(isodata-gen-new-fn-verify-guards-hints-nonpred appcond-thm-names old$ arg-isomaps res-isomaps new$ old-to-new$ old-fn-unnorm-name newp-of-new$ wrld) → hints
Function:
(defun isodata-gen-new-fn-verify-guards-hints-nonpred (appcond-thm-names old$ arg-isomaps res-isomaps new$ old-to-new$ old-fn-unnorm-name newp-of-new$ 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-to-new$) (symbolp old-fn-unnorm-name) (symbolp newp-of-new$) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-new-fn-verify-guards-hints-nonpred)) (declare (ignorable __function__)) (if (recursivep old$ nil wrld) (if (consp res-isomaps) (isodata-gen-new-fn-verify-guards-hints-nonpred-rec-1res/mres appcond-thm-names old$ arg-isomaps res-isomaps new$ old-to-new$ old-fn-unnorm-name newp-of-new$ wrld) (isodata-gen-new-fn-verify-guards-hints-nonpred-rec-0res appcond-thm-names old$ arg-isomaps old-to-new$ wrld)) (if (consp res-isomaps) (isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-1res/mres appcond-thm-names old$ arg-isomaps res-isomaps old-fn-unnorm-name wrld) (isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res old$ arg-isomaps wrld)))))