Consider the TRS R consisting of the rewrite rules

1: x - 0 -> x
2: 0 - s(y) -> 0
3: s(x) - s(y) -> x - y
4: f(0) -> 0
5: f(s(x)) -> s(x) - g(f(x))
6: g(0) -> s(0)
7: g(s(x)) -> s(x) - f(g(x))

There are 7 dependency pairs:

8: s(x) -# s(y) -> x -# y
9: F(s(x)) -> s(x) -# g(f(x))
10: F(s(x)) -> G(f(x))
11: F(s(x)) -> F(x)
12: G(s(x)) -> s(x) -# f(g(x))
13: G(s(x)) -> F(g(x))
14: G(s(x)) -> G(x)

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

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

- Consider the SCC {10,11,13,14}.
By taking the polynomial interpretation
[0] = 1
and [-](x,y) = [f](x) = [F](x) = [g](x) = [G](x) = [s](x) = x + 1,
the rules in {5-7,10,13}
are weakly decreasing and
the rules in {1-4,11,14}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {10,13}.
By taking the polynomial interpretation
[0] = 1,
[-](x,y) = [f](x) = x
and [F](x) = [g](x) = [G](x) = [s](x) = x + 1,
the rules in {1,2,4-6,13}
are weakly decreasing and
the rules in {3,7,10}
are strictly decreasing.


Hence the TRS is terminating.