Tthm
The measure (termination) theorem for a given function symbol
Example Forms:
:tthm FN
(tthm 'FN) ; equivalent to the above
where FN is a function symbol. This shows the measure (termination) theorem for FN. More precisely, evaluation of a
call of this macro — pronounced ``tee-thumb'' — either results in
an error or returns an error-triple whose value component is the
user-level (untranslated) version of that termination theorem. Also see lemma-instance for discussion of a related :termination-theorem prover
hint.
Technical note: a corresponding evaluation that provides a (translated)
termp is: (termination-theorem 'FN (w state)).
