Generate the hints to prove the theorem that expresses the new function in terms of the old function, when the functions are not recursive.
(expdata-gen-new-to-old-thm-hints-nonrec old-fn-unnorm-name new-fn-unnorm-name) → hints
Function:
(defun expdata-gen-new-to-old-thm-hints-nonrec (old-fn-unnorm-name new-fn-unnorm-name) (declare (xargs :guard (and (symbolp old-fn-unnorm-name) (symbolp new-fn-unnorm-name)))) (let ((__function__ 'expdata-gen-new-to-old-thm-hints-nonrec)) (declare (ignorable __function__)) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-fn-unnorm-name (cons new-fn-unnorm-name 'nil)) 'nil)) 'nil))) 'nil)))
Theorem:
(defthm true-listp-of-expdata-gen-new-to-old-thm-hints-nonrec (b* ((hints (expdata-gen-new-to-old-thm-hints-nonrec old-fn-unnorm-name new-fn-unnorm-name))) (true-listp hints)) :rule-classes :rewrite)