Consider the TRS R consisting of the rewrite rules

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

There are 7 dependency pairs:

7: MINUS(s(x),s(y)) -> MINUS(x,y)
8: F(s(x)) -> MINUS(s(x),g(f(x)))
9: F(s(x)) -> G(f(x))
10: F(s(x)) -> F(x)
11: G(s(x)) -> MINUS(s(x),f(g(x)))
12: G(s(x)) -> F(g(x))
13: G(s(x)) -> G(x)

The approximated dependency graph contains 2 SCCs:
{7}
and {9,10,12,13}.

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

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

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


Hence the TRS is terminating.