Consider the TRS R consisting of the rewrite rules

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

There are 5 dependency pairs:

4: x +# (y + z) -> (x + y) +# z
5: x +# (y + z) -> x +# y
6: (x * y) +# (x + 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-8}.

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

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


Hence the TRS is terminating.