## A Sketch of How the Rewriter Works

Below we show the first target term, extracted from the
current conjecture. Below it we show the associativity rule.

The variables of the rewrite rule are **instantiated** so that the
**left-hand side** of the rule matches the target:

variable term from target
a x1
b x2
c (app x3 x4)

Then the target is **replaced** by the instantiated **right-hand side**
of the rule.

Sometimes rules have **hypotheses**. To make a long story short,
if the rule has hypotheses, then after matching the left-hand side,
the rewriter instantiates the hypotheses and rewrites them recursively.
This is called **backchaining**. If they all rewrite to true, then
the target is replaced as above.

For more details on how the ACL2 rewriter works, see Boyer and Moore's
book **A Computational Logic**, Academic Press, 1979.