Enhanced variant of induction-machine.
(induction-machine+ fn wrld) → result
This returns the same result as induction-machine,
but it includes a run-time check (which should always succeed) on the result
that allows us to prove the return type theorem
without strengthening the guard on
(defun induction-machine+ (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'induction-machine+)) (declare (ignorable __function__)) (if (not (= (len (irecursivep+ fn wrld)) 1)) (raise "The function ~x0 is not singly recursive." fn) (b* ((result (induction-machine fn wrld))) (if (pseudo-tests-and-calls-listp result) result (raise "Internal error: ~ the INDUCTION-MACHINE property ~x0 of ~x1 ~ does not have the expected form." result fn))))))
(defthm pseudo-tests-and-calls-listp-of-induction-machine+ (b* ((result (induction-machine+ fn wrld))) (pseudo-tests-and-calls-listp result)) :rule-classes :rewrite)