Consider the TRS R consisting of the rewrite rules

1: x + 0 -> x
2: x + s(y) -> s(x + y)
3: 0 + y -> y
4: s(x) + y -> s(x + y)
5: x + (y + z) -> (x + y) + z
6: f(g(f(x))) -> f(h(s(0),x))
7: f(g(h(x,y))) -> f(h(s(x),y))
8: f(h(x,h(y,z))) -> f(h(x + y,z))

There are 8 dependency pairs:

9: x +# s(y) -> x +# y
10: s(x) +# y -> x +# y
11: x +# (y + z) -> (x + y) +# z
12: x +# (y + z) -> x +# y
13: F(g(f(x))) -> F(h(s(0),x))
14: F(g(h(x,y))) -> F(h(s(x),y))
15: F(h(x,h(y,z))) -> F(h(x + y,z))
16: F(h(x,h(y,z))) -> x +# y

The approximated dependency graph contains 2 SCCs:
{9-12}
and {15}.

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

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


- Consider the SCC {15}.
The usable rules are {1-5}.
By taking the polynomial interpretation
[0] = 1,
[F](x) = [s](x) = x + 1,
[+](x,y) = x + y + 1
and [h](x,y) = y + 1,
the rules in {2,4,5}
are weakly decreasing and
the rules in {1,3,15}
are strictly decreasing.

Hence the TRS is terminating.