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.

suggested by this conjecture.  Subsumption reduces that number to two.

                 (:P (CDR A) B C))
            (:P A B C))
scheme produces the following two nontautological subgoals.