Consider the TRS R consisting of the rewrite rules

1: a + b -> b + a
2: a + (b + z) -> b + (a + z)
3: (x + y) + z -> x + (y + z)
4: f(a,y) -> a
5: f(b,y) -> b
6: f(x + y,z) -> f(x,z) + f(y,z)

There are 8 dependency pairs:

7: a +# b -> b +# a
8: a +# (b + z) -> b +# (a + z)
9: a +# (b + z) -> a +# z
10: (x + y) +# z -> x +# (y + z)
11: (x + y) +# z -> y +# z
12: F(x + y,z) -> f(x,z) +# f(y,z)
13: F(x + y,z) -> F(x,z)
14: F(x + y,z) -> F(y,z)

The approximated dependency graph contains 3 SCCs:
{9},
{10,11}
and {13,14}.

- Consider the SCC {9}.
There are no usable rules.
By taking the polynomial interpretation
[a] = [b] = 1
and [+](x,y) = [+#](x,y) = x + y + 1,
rule 9
is strictly decreasing.

- Consider the SCC {10,11}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[a] = [b] = 1
and [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {1-3,10}
are weakly decreasing and
rule 11
is strictly decreasing.
There is one new SCC.

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


- Consider the SCC {13,14}.
There are no usable rules.
By taking the polynomial interpretation
[+](x,y) = [F](x,y) = x + y + 1,
the rules in {13,14}
are strictly decreasing.

Hence the TRS is terminating.