Generate the hints to verify the guards of the new function.
(expdata-gen-new-fn-verify-guards-hints appcond-thm-names old$ arg-surjmaps res-surjmaps predicate$ new-to-old$ new$ old-to-new$ old-fn-unnorm-name newp-of-new$ wrld) → hints
Function:
(defun expdata-gen-new-fn-verify-guards-hints (appcond-thm-names old$ arg-surjmaps res-surjmaps predicate$ new-to-old$ 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) (booleanp predicate$) (symbolp new-to-old$) (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)) (declare (ignorable __function__)) (if predicate$ (expdata-gen-new-fn-verify-guards-hints-pred appcond-thm-names old$ arg-surjmaps new-to-old$ wrld) (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))))