Consider the TRS R consisting of the rewrite rules

1: (x * y) + (x * z) -> x * (y + z)
2: (x + y) + z -> x + (y + z)
3: (x * y) + ((x * z) + u) -> (x * (y + z)) + u

There are 5 dependency pairs:

4: (x * y) +# (x * z) -> y +# z
5: (x + y) +# z -> x +# (y + z)
6: (x + y) +# z -> y +# z
7: (x * y) +# ((x * z) + u) -> (x * (y + z)) +# u
8: (x * y) +# ((x * z) + u) -> y +# z

The approximated dependency graph contains one SCC:
{4-6,8}.

- Consider the SCC {4-6,8}.
By taking the polynomial interpretation
[u] = 1
and [*](x,y) = [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {2,5}
are weakly decreasing and
the rules in {1,3,4,6,8}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {5}.
By taking the polynomial interpretation
[u] = 1,
[+#](x,y) = x + 1
and [*](x,y) = [+](x,y) = x + y + 1,
rule 2
is weakly decreasing and
the rules in {1,3,5}
are strictly decreasing.


Hence the TRS is terminating.