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.