The Theorem that App is Associative
ACL2!>(defthm associativity-of-app (equal (app (app a b) c) (app a (app b c))))
The formula above says
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.