### LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-EVALUATION

evaluation during proofs
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

Any time you are proving a formula and see a subterm in the formula
that contains no variables, you can just evaluate the subterm.

This is familiar from algebra: It is not uncommon to
rearrange a polynominal to collect all the constants and
then add them up:

(3x + 2 + 7y + 2)
=
(3x + 7y + (2 + 2))
=
(3x + 7y + 4).

That last step is just evaluation.
It happens often in ACL2 proofs because theorems involve constants
and defined functions and when those constants ``drift into the maw''
of a function, the function call can be eliminated and replaced by
a new constant. ACL2 does this automatically; you don't have to tell it.
In fact, there are a few occasions where you might prefer it *not*
evaluate and those are the ones you have to look out for! They'll be
obvious when they happen because you'll see a mysterious constant crop
up in the proof.

Evaluation is legal because it is just the repeated use of
unconditional rewriting to replace definitions by their instantiated
bodies until no function calls remain.

Now use your browser's **Back Button** to return to the example proof in
logic-knowledge-taken-for-granted.