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)))))
