### EXAMPLE-INDUCTION-SCHEME-WITH-ACCUMULATORS

induction scheme with accumulators
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

See logic-knowledge-taken-for-granted-inductive-proof for an explanation of
what we mean by the induction *suggested* by a recursive function or a
term.

To prove `(p x a)`

for all `x`

and all `a`

, prove each of the following:

*Base Case*:
(implies (endp x)
(p x a))

*Induction Step*:
(implies (and (not (endp x))
(p (cdr x) (cons (car x) a)))
(p x a))

Note that in the induction hypothesis we assume `p`

for a smaller `x`

but
a larger `a`

. In fact, we could include as many induction hypotheses as we
want and use any terms we want in the `a`

position as long as the `x`

position is occupied by a smaller term.
A function that suggests this particular induction is shown below.

(defun rev1 (x a)
(if (endp x)
a
(rev1 (cdr x) (cons (car x) a)))).

A function that suggests a similar induction in which three induction hypotheses are
provided, one in which the `a`

position is occupied by `(cons (car x) a)`

,
another in which the `a`

position is occupied by some arbitrary term `b`

,
and a third in which the `a`

position is occupied by `a`

, is suggested by
the term `(rev1-modified x a b)`

where

(defun rev1-modified (x a b)
(if (endp x)
(list x a b)
(list (rev1-modified (cdr x) (cons (car x) a) b)
(rev1-modified (cdr x) b b)
(rev1-modified (cdr x) a b))))

Remember that the value of this term or function is irrelevant to the induction
suggested. Because ACL2's definitional principle insists that all the formal
parameters play a role in the computation (at least syntactically), it is common
practice when defining functions for their induction schemes to return the
`list`

of all the formals (to insure all variables are involved) and to combine
recursive calls on a given branch with `list`

(to avoid introducing additional
case analysis as would happen if `and`

or `or`

or other propositional functions
are used).
If you tried to prove `(p x a)`

and suggested the induct hint
`(rev1-modified x a (fact k))`

, as by

(thm (p x a)
:hints (("Goal" :induct (rev1-modified x a (fact k)))))

the inductive argument would be:
*Base Case*:
(implies (endp x)
(p x a))

*Inductive Step*:
(implies (and (not (endp x))
(p (cdr x) (cons (car x) a))
(p (cdr x) (fact k))
(p (cdr x) a))
(p x a))