## 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 `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.