Consider the TRS R consisting of the rewrite rules

1: pred(s(x)) -> x
2: minus(x,0) -> x
3: minus(x,s(y)) -> pred(minus(x,y))
4: quot(0,s(y)) -> 0
5: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))

There are 4 dependency pairs:

6: MINUS(x,s(y)) -> PRED(minus(x,y))
7: MINUS(x,s(y)) -> MINUS(x,y)
8: QUOT(s(x),s(y)) -> QUOT(minus(x,y),s(y))
9: QUOT(s(x),s(y)) -> MINUS(x,y)

The approximated dependency graph contains 2 SCCs:
{7}
and {8}.

- 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 {8}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[0] = 1,
[minus](x,y) = [pred](x) = x,
[s](x) = x + 1
and [QUOT](x,y) = x + y + 1,
the rules in {2,3}
are weakly decreasing and
the rules in {1,8}
are strictly decreasing.

Hence the TRS is terminating.