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