Create a copy of a function's termination theorem that calls stubs.

The `termination-theorem` lemma-instance
provides a way to re-use a recursive definition's termination (measure)
theorem. You might find it convenient, however, to create a

The form `rule-classes`

(defun f (x) (if (consp x) (and (f (caar x)) (f (cddr x))) x))

Here is the termination-theorem for

ACL2 !>:tthm f (AND (O-P (ACL2-COUNT X)) (OR (NOT (CONSP X)) (O< (ACL2-COUNT (CAR (CAR X))) (ACL2-COUNT X))) (OR (NOT (CONSP X)) (NOT (F (CAR (CAR X)))) (O< (ACL2-COUNT (CDDR X)) (ACL2-COUNT X)))) ACL2 !>

We now create the corresponding

ACL2 !>(make-termination-theorem f) Summary Form: ( MAKE-EVENT (ER-LET* ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) (DEFTHM F$TTHM (AND (O-P (ACL2-COUNT X)) (OR (NOT (CONSP X)) (O< (ACL2-COUNT (CAR (CAR X))) (ACL2-COUNT X))) (OR (NOT (CONSP X)) (NOT (F$STUB (CAR (CAR X)))) (O< (ACL2-COUNT (CDDR X)) (ACL2-COUNT X)))) :HINTS (("Goal" :USE (:TERMINATION-THEOREM F ((F F$STUB))) :IN-THEORY (THEORY 'MINIMAL-THEORY))) :RULE-CLASSES NIL) ACL2 !>

Notice that the call of `defstub`, which has
no constraints, thus easing the application of functional-instantiation
to this theorem.

General Form: (make-termination-theorem Fun :subst S ; default described below :thm-name N ; default Fun$TTHM :rule-classes R ; default nil :verbose Vflg ; default nil :show-only Sflg ; default nil )

where no keyword argument is evaluated unless wrapped in `defthm` event based
on the termination-theorem of

Fun is a function symbol defined by recursion (possibly`mutual-recursion`).S is a functional substitution, that is, a list of 2-element lists of symbols(fi gi) . For each symbolgi that is not a function symbol in the current world, a suitable`defstub`event will be introduced forgi . IfFun is singly recursive then there will be a single such pair(Fun g) ; otherwiseFun is defined by`mutual-recursion`and eachfi must have been defined together withFun , in the samemutual-recursion form. If:subst is omitted then each suitable function symbolf — that is,Fun as well as, in the case of mutual recursion, the others defined withFun — is paired with the result of adding the suffix"$STUB" to the symbol-name off .R is the: `rule-classes`argument of the generateddefthm event.- Output is mostly suppressed by default, but is enabled when
Vflg is notnil . - If
Sflg is notnil , then the generateddefthm eventEV will not be submitted; instead, it will be returned in an error-triple(mv nil EV state) .