## The Associativity of App

ACL2!>**(let ((a '(1 2))**
**(b '(3 4))**
**(c '(5 6)))**
**(equal (app (app a b) c)**
**(app a (app b c))))**
T

Observe that, for the particular `a`

, `b`

, and `c`

above,
`(app (app a b) c)`

returns the same thing as `(app a (app b c))`

.
Perhaps `app`

is **associative**. Of course, to be associative means
that the above property must hold for all values of `a`

, `b`

, and `c`

,
not just the ones **tested** above.

Wouldn't it be cool if you could type

ACL2!>**(equal (app (app a b) c)**
**(app a (app b c)))**

and have ACL2 compute the value `T`

? Well, **you can't!** If you try
it, you'll get an error message! The message says we can't evaluate
that form because it contains **free** variables, i.e., variables
not given values. Click here to see the
message.
We cannot evaluate a form on an infinite number of cases. But we can
prove that a form is a theorem and hence know that it will always
evaluate to true.