to the associativity of .That rule can be applied at the numerator in the term with the matching substitution , see picture 2. Applying that substitution to the rule's right-hand side yields the term , and replacing the numerator by that term yields , which is the result term of applying the rewrite rule. Altogether, applying the rewrite rule has achieved what is called "applying the associativity law for to " in elementary algebra. Alternately, the rule could have been applied to the denominator of the original term, yielding .

Termination