## The Proof of the Associativity of App

Here is the theorem prover's output when it processes the **defthm**
command for the associativity of `app`

. We have highlighted text
for which we offer some explanation, and broken the presentation into
several pages. Just follow the Walking Tour after exploring the
explanations.

ACL2!>**(defthm associativity-of-app**
**(equal (app (app a b) c)**
**(app a (app b c))))**
Name the formula above *1.

Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.

We will induct according to a scheme suggested by (APP A B). If we
let (:P A B C) denote *1 above then the induction scheme we'll use
is
(AND
(IMPLIES (AND (NOT (ENDP A))
(:P (CDR A) B C))
(:P A B C))
(IMPLIES (ENDP A) (:P A B C))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.