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