Generate the hints to verify the guards of the new function,
when recursive and when
(expdata-gen-new-fn-verify-guards-hints-pred-rec appcond-thm-names old$ arg-surjmaps new-to-old$ wrld) → hints
This is according to the design notes, taking into account that there may be multiple recursive calls, while the design notes only assume one.
Function:
(defun expdata-gen-new-fn-verify-guards-hints-pred-rec (appcond-thm-names old$ arg-surjmaps new-to-old$ wrld) (declare (xargs :guard (and (symbol-symbol-alistp appcond-thm-names) (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (symbolp new-to-old$) (plist-worldp wrld)))) (let ((__function__ 'expdata-gen-new-fn-verify-guards-hints-pred-rec)) (declare (ignorable __function__)) (b* ((rec-calls (recursive-calls old$ wrld)) (oldp-of-rec-call-args (cdr (assoc-eq :oldp-of-rec-call-args appcond-thm-names))) (old-guard-pred (cdr (assoc-eq :old-guard-pred appcond-thm-names))) (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-forth-guard-instances-to-x1...xn 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-old-guard-pred (expdata-gen-lemma-instance-x1...xn-to-back-of-x1...xn old-guard-pred 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-new-to-old (expdata-gen-lemma-instances-x1...xn-to-forth-rec-call-args-back new-to-old$ rec-calls old$ arg-surjmaps 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-old-guard-pred (cons instance-oldp-of-rec-call-args instances-new-to-old))))))))) 'nil))))) 'nil))))