Induction scheme with accumulators

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

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

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

(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

If you tried to prove

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