Consider the TRS R consisting of the rewrite rules

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

There are 3 dependency pairs:

3: F(x + 0) -> F(x)
4: x +# (y + z) -> (x + y) +# z
5: x +# (y + z) -> x +# y

The approximated dependency graph contains 2 SCCs:
{4,5}
and {3}.

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

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


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

Hence the TRS is terminating.