Minimize the ruler-extenders necessary to admit a definition.

`defun` or `defund`
form by declaring a minimal set of ruler-extenders. This MIN_NEW
utility uses proof to eliminate ruler-extenders as completely as possible,
while still permitting the termination proof to succeed. The second utility,
which we call MIN_OLD below, is applied to a function symbol that already has
a recursive (but not mutually recursive) definition. Here are examples that
illustrate each of these two respective utilities.

; MIN_NEW (to admit a proposed definition): (minimize-ruler-extenders (defun foo (x) (car (if (endp x) x (cons (foo (cdr x)) (evens (if (consp (cdr x)) (foo (cddr x)) nil))))))) ; MIN_OLD (to compute minimal ruler-extenders for an existing definition): (defun bar (x) (declare (xargs :ruler-extenders :all)) (mod (if (consp x) (* (bar (car x)) (if (consp (cdr x)) (ifix (cadr x)) 17)) 3) 23)) (minimize-ruler-extenders bar) ; returns (MOD)

In the first (MIN_NEW) example above, a minimal set of ruler-extenders — in fact, THE minimal set — is the set

ACL2 !>:pe foo L 2:x(MINIMIZE-RULER-EXTENDERS (DEFUN FOO # ...)) \ >L (DEFUN FOO (X) (DECLARE (XARGS :RULER-EXTENDERS (CAR))) (CAR (IF (ENDP X) X (CONS (FOO (CDR X)) (EVENS (IF (CONSP (CDR X)) (FOO (CDDR X)) NIL)))))) ACL2 !>

The input form for the MIN_NEW utility should be a call of `defun` or
`defund` that defines a function symbol that is not already defined. If
that form specifies `xargs` declaration,

Now we turn to the MIN_OLD utility. This utility is applied to a function
symbol