A logic-mode guard-verified version of
the built-in

We use `magic-ev-fncall` to call `magic-ev-fncall` fails,
or if the result is not a symbol,
we also stop with hard errors.

Compared to `magic-ev-fncall` overhead.
However, it can be used in logic-mode guard-verified code
that follows a statically typed discipline.

**Function: **

(defun termination-theorem$ (fn state) (declare (xargs :stobjs (state))) (declare (xargs :guard (symbolp fn))) (declare (xargs :guard (and (function-symbolp fn (w state)) (logicp fn (w state))))) (let ((__function__ 'termination-theorem$)) (declare (ignorable __function__)) (b* (((mv erp term?) (magic-ev-fncall 'termination-theorem (list fn (w state)) state nil t)) ((when erp) (raise "Internal error: ~@0" term?) (cons :failed "")) ((unless (and (consp term?) (or (and (equal (car term?) :failed) (msgp (cdr term?))) (and (not (equal (car term?) :failed)) (pseudo-termp term?))))) (raise "Internal error: ~x0 is malformed." term?) (cons :failed ""))) term?)))

**Theorem: **

(defthm return-type-of-termination-theorem$ (b* ((term? (termination-theorem$ fn state))) (or (and (consp term?) (equal (car term?) :failed) (msgp (cdr term?))) (symbolp term?) (and (consp term?) (not (equal (car term?) :failed)) (pseudo-termp term?)))) :rule-classes :rewrite)

**Theorem: **

(defthm consp-of-termination-theorem$ (b* ((term? (termination-theorem$ fn state))) (consp term?)) :rule-classes :type-prescription)

**Theorem: **

(defthm msgp-of-termination-theorem-when-failed (b* ((?term? (termination-theorem$ fn state))) (implies (equal (car term?) :failed) (msgp (cdr term?)))))

**Theorem: **

(defthm msgp-of-termination-theorem-when-not-failed (b* ((?term? (termination-theorem$ fn state))) (implies (not (equal (car term?) :failed)) (pseudo-termp term?))))