Generate the hints to verify the guards of the new function,
when the function is recursive,
when
(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) → hints
Function:
(defun 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) (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)))) (declare (xargs :guard (consp res-surjmaps))) (let ((__function__ 'expdata-gen-new-fn-verify-guards-hints-nonpred-rec-1res/mres)) (declare (ignorable __function__)) (b* ((oldp-of-old (cdr (assoc-eq :oldp-of-old appcond-thm-names))) (oldp-of-rec-call-args (cdr (assoc-eq :oldp-of-rec-call-args appcond-thm-names))) (rec-calls (recursive-calls old$ wrld)) (instance-guard-thm-old (expdata-gen-lemma-instance-x1...xn-to-back-of-x1...xn (cons ':guard-theorem (cons old$ 'nil)) old$ arg-surjmaps wrld)) (instances-newp-guard (expdata-gen-newp-guard-instances-to-x1...xn arg-surjmaps wrld)) (instances-forth-guard (expdata-gen-all-forth-guard-instances-to-terms-back rec-calls old$ arg-surjmaps wrld)) (instances-back-guard (expdata-gen-back-guard-instances-to-x1...xn arg-surjmaps wrld)) (instances-forth-image (expdata-gen-all-forth-image-instances-to-terms-back rec-calls old$ arg-surjmaps wrld)) (instances-back-image (expdata-gen-back-image-instances-to-x1...xn arg-surjmaps wrld)) (instances-back-of-forth (expdata-gen-all-back-of-forth-instances-to-terms-back rec-calls old$ arg-surjmaps wrld)) (instance-oldp-of-rec-call-args (expdata-gen-lemma-instance-x1...xn-to-back-of-x1...xn oldp-of-rec-call-args old$ arg-surjmaps wrld)) (instances-old-to-new (expdata-gen-lemma-instances-x1...xn-to-rec-call-args-back old-to-new$ rec-calls old$ arg-surjmaps wrld)) (instance-oldp-of-old (expdata-gen-lemma-instance-x1...xn-to-back-of-x1...xn oldp-of-old old$ arg-surjmaps wrld)) (instance-old-fn-unnorm-name (expdata-gen-lemma-instance-x1...xn-to-back-of-x1...xn old-fn-unnorm-name old$ arg-surjmaps wrld)) (instances-newp-of-new (expdata-gen-lemma-instances-x1...xn-to-forth-rec-call-args-back newp-of-new$ rec-calls old$ arg-surjmaps wrld)) (x1...xn (formals old$ wrld)) (old-call (fcons-term old$ x1...xn)) (back-of-x1...xn (expdata-gen-back-of-terms x1...xn arg-surjmaps)) (old-call-of-back-x1...xn (subcor-var x1...xn back-of-x1...xn old-call)) (instances-forth-guard-res (if (= (len res-surjmaps) 1) (b* ((res-surjmap (cdar res-surjmaps)) (forth-guard-res (expdata-surjmap->forth-guard res-surjmap)) (var (expdata-formal-of-forth res-surjmap wrld))) (cons (cons ':instance (cons forth-guard-res (cons ':extra-bindings-ok (cons (cons var (cons old-call-of-back-x1...xn 'nil)) 'nil)))) 'nil)) (expdata-gen-forth-guard-instances-to-mv-nth old-call-of-back-x1...xn res-surjmaps wrld))) (instances-back-guard-res (if (= (len res-surjmaps) 1) (b* ((res-surjmap (cdar res-surjmaps)) (back-guard-res (expdata-surjmap->back-guard res-surjmap)) (var (expdata-formal-of-back res-surjmap wrld))) (expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back back-guard-res var rec-calls old$ arg-surjmaps new$ wrld)) (expdata-gen-all-back-guard-instances-to-mv-nth old$ rec-calls arg-surjmaps res-surjmaps new$ wrld)))) (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (append instances-newp-guard (append instances-forth-guard (append instances-back-guard (append instances-forth-image (append instances-back-image (append instances-back-of-forth (cons instance-guard-thm-old (cons instance-oldp-of-rec-call-args (append instances-old-to-new (cons instance-oldp-of-old (cons instance-old-fn-unnorm-name (append instances-newp-of-new (append instances-forth-guard-res instances-back-guard-res))))))))))))) 'nil))))) 'nil))))