Generate the hints to verify the guards of the new function,
when the function is not recursive,
when
(isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res old$ arg-isomaps wrld) → hints
Function:
(defun isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res (old$ arg-isomaps wrld) (declare (xargs :guard (and (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res)) (declare (ignorable __function__)) (b* ((instance-guard-thm-old (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn (cons ':guard-theorem (cons old$ 'nil)) old$ arg-isomaps wrld)) (instances-newp-guard (isodata-gen-newp-guard-instances-to-x1...xn arg-isomaps wrld)) (instances-back-guard (isodata-gen-back-guard-instances-to-x1...xn arg-isomaps wrld))) (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (cons instance-guard-thm-old (append instances-newp-guard instances-back-guard)) 'nil))))) 'nil))))
Theorem:
(defthm true-listp-of-isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res (b* ((hints (isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res old$ arg-isomaps wrld))) (true-listp hints)) :rule-classes :rewrite)