Consider the TRS R consisting of the rewrite rules

1: minus(X,0) -> X
2: minus(s(X),s(Y)) -> p(minus(X,Y))
3: p(s(X)) -> X
4: div(0,s(Y)) -> 0
5: div(s(X),s(Y)) -> s(div(minus(X,Y),s(Y)))

There are 4 dependency pairs:

6: MINUS(s(X),s(Y)) -> P(minus(X,Y))
7: MINUS(s(X),s(Y)) -> MINUS(X,Y)
8: DIV(s(X),s(Y)) -> DIV(minus(X,Y),s(Y))
9: DIV(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) = x,
[p](x) = [s](x) = x + 1
and [DIV](x,y) = x + y + 1,
the rules in {1,2}
are weakly decreasing and
the rules in {3,8}
are strictly decreasing.

Hence the TRS is terminating.