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)))

There are 3 dependency pairs:

5: MINUS(s(x),s(y)) -> MINUS(x,y)
6: QUOT(s(x),s(y)) -> QUOT(minus(x,y),s(y))
7: QUOT(s(x),s(y)) -> MINUS(x,y)

The approximated dependency graph contains 2 SCCs:
{5}
and {6}.

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

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

Hence the TRS is terminating.