## 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. (The
most recent version of ACL2 may print slightly different output but the
basics are the same.) Just follow the Walking Tour after exploring the
explanations.

However, before exploring this output you should understand that ACL2 users
rarely read successful proofs! Instead, they look at certain subgoals
printed in failed proofs, figure whether and how those subgoals can be
proved, and give ACL2 directions for proving them, usually by simply proving
other lemmas. Furthermore, to be a good user of ACL2 you do not have to
understand how the theorem prover works. You just have to understand how to
interact with it. We explain this in great detail later. But basically all
new users are curious to know how ACL2 works and this little tour attempts to
give some answers, just to satisfy your curiosity.

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
O< (which is known to be well-founded on the domain recognized
by O-P). When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.