## 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.

We discuss the rewriter in more detail in the extended introduction to how to
use the theorem prover, see introduction-to-the-theorem-prover, which we
will recommend you work through **after** you have finished the two tours.