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))
```