Consider the TRS R consisting of the rewrite rules

1: minus(x,0) -> x
2: minus(s(x),s(y)) -> minus(x,y)
3: quot(0,s(y)) -> 0
4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
5: plus(0,y) -> y
6: plus(s(x),y) -> s(plus(x,y))
7: minus(minus(x,y),z) -> minus(x,plus(y,z))

There are 6 dependency pairs:

8: MINUS(s(x),s(y)) -> MINUS(x,y)
9: QUOT(s(x),s(y)) -> QUOT(minus(x,y),s(y))
10: QUOT(s(x),s(y)) -> MINUS(x,y)
11: PLUS(s(x),y) -> PLUS(x,y)
12: MINUS(minus(x,y),z) -> MINUS(x,plus(y,z))
13: MINUS(minus(x,y),z) -> PLUS(y,z)

The approximated dependency graph contains 3 SCCs:
{11},
{8,12}
and {9}.

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

- Consider the SCC {8,12}.
The usable rules are {5,6}.
By taking the polynomial interpretation
[0] = 1,
[s](x) = x + 1
and [minus](x,y) = [MINUS](x,y) = [plus](x,y) = x + y + 1,
the rules in {6,12}
are weakly decreasing and
the rules in {5,8}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {12}.
By taking the polynomial interpretation
[0] = 1,
[MINUS](x,y) = [s](x) = x + 1
and [minus](x,y) = [plus](x,y) = x + y + 1,
rule 6
is weakly decreasing and
the rules in {5,12}
are strictly decreasing.


- Consider the SCC {9}.
The usable rules are {1,2,5-7}.
By taking the polynomial interpretation
[0] = 1,
[minus](x,y) = x,
[s](x) = x + 1
and [plus](x,y) = [QUOT](x,y) = x + y + 1,
the rules in {1,6,7}
are weakly decreasing and
the rules in {2,5,9}
are strictly decreasing.

Hence the TRS is terminating.