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.