Consider the TRS R consisting of the rewrite rules

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

There are 5 dependency pairs:

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

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

- Consider the SCC {4-8}.
By taking the polynomial interpretation
[f](x) = x + 1
and [+](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) = [f](x) = x + 1
and [+](x,y) = x + y + 1,
rule 1
is weakly decreasing and
the rules in {2-4}
are strictly decreasing.


Hence the TRS is terminating.