## Analyzing Common Lisp Models

To analyze a model you must be able to reason about the operations and
relations involved. Perhaps, for example, some aspect of the model depends
upon the fact that the concatenation operation is associative.

In any Common Lisp you can confirm that

(app '(A B) (app '(C D) '(E F)))

and
(app (app '(A B) '(C D)) '(E F)))

both evaluate to the same thing, `(A B C D E F)`

.But what distinguishes ACL2 (the logic) from applicative Common Lisp (the
language) is that in ACL2 you can **prove** that the concatenation function
`app`

is associative when its arguments are true-lists, whereas in Common
Lisp all you can do is test that proposition.

That is, in ACL2 it makes sense to say that the following formula is a
``theorem.''

**Theorem** Associativity of App
(implies (and (true-listp a)
(true-listp b))
(equal (app (app a b) c)
(app a (app b c))))

Theorems about the properties of models are proved by symbolically
manipulating the operations and relations involved. If the concatenation of
sequences is involved in your model, then you may well need the theorem above
in order to that your model has some particular property.