The First Application of the Associativity Rule

So here we see our associativity rule being used!

The rewriter sweeps the conjecture in a leftmost innermost fashion, applying rewrite rules as it goes.

The associativity rule is used many times in this sweep. The first ``target'' is highlighted below. Click on it to see what happens:

Current Conjecture:
(equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
       (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))