## Proving Theorems about Models

But ACL2 is a **logic**. We can **prove theorems about the model**.

**Theorem. MC 'mult is a multiplier**
(implies (and (natp x)
(natp y))
(equal (lookup 'z (mc (s 'mult x y) (mclk x)))
(* x y))).

This theorem says that a certain program running on the **mc** machine
will correctly multiply **any two natural numbers**.

It is a statement about an **infinite** number of test cases!

We know it is true about the model because we **proved** it.