ACL2!>(defthm associativity-of-app
(equal (app (app a b) c)
(app a (app b c))))
The formula above says app is associative. The defthm 
command instructs ACL2 to prove the formula and to name it
associativity-of-app. Actually, the defthm command also builds the
formula into the database as a rewrite rule, but we won't go
into that just yet.
What we will consider is how the ACL2 theorem prover proves this formula.
If you proceed you will find the actual output of ACL2 in response to the command above. Some of the text is highlighted for the purposes of the tour. ACL2 does not highlight its output.
You will note that we sometimes highlight a single open parenthesis. This is our way of drawing your attention to the subformula that begins with that parenthesis. By clicking on the parenthesis you will get an explanation of the subformula or its processing.
