Consider the TRS R consisting of the rewrite rules

1: minus(0,Y) -> 0
2: minus(s(X),s(Y)) -> minus(X,Y)
3: geq(X,0) -> true
4: geq(0,s(Y)) -> false
5: geq(s(X),s(Y)) -> geq(X,Y)
6: div(0,s(Y)) -> 0
7: div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
8: if(true,X,Y) -> X
9: if(false,X,Y) -> Y

There are 6 dependency pairs:

10: MINUS(s(X),s(Y)) -> MINUS(X,Y)
11: GEQ(s(X),s(Y)) -> GEQ(X,Y)
12: DIV(s(X),s(Y)) -> IF(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
13: DIV(s(X),s(Y)) -> GEQ(X,Y)
14: DIV(s(X),s(Y)) -> DIV(minus(X,Y),s(Y))
15: DIV(s(X),s(Y)) -> MINUS(X,Y)

The approximated dependency graph contains 3 SCCs:
{11},
{10}
and {14}.

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

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

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

Hence the TRS is terminating.