Consider the TRS R consisting of the rewrite rules

1: minus(n__0,Y) -> 0
2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
3: geq(X,n__0) -> true
4: geq(n__0,n__s(Y)) -> false
5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
6: div(0,n__s(Y)) -> 0
7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0)
8: if(true,X,Y) -> activate(X)
9: if(false,X,Y) -> activate(Y)
10: 0 -> n__0
11: s(X) -> n__s(X)
12: activate(n__0) -> 0
13: activate(n__s(X)) -> s(X)
14: activate(X) -> X

There are 16 dependency pairs:

15: MINUS(n__0,Y) -> 0#
16: MINUS(n__s(X),n__s(Y)) -> MINUS(activate(X),activate(Y))
17: MINUS(n__s(X),n__s(Y)) -> ACTIVATE(X)
18: MINUS(n__s(X),n__s(Y)) -> ACTIVATE(Y)
19: GEQ(n__s(X),n__s(Y)) -> GEQ(activate(X),activate(Y))
20: GEQ(n__s(X),n__s(Y)) -> ACTIVATE(X)
21: GEQ(n__s(X),n__s(Y)) -> ACTIVATE(Y)
22: DIV(s(X),n__s(Y)) -> IF(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0)
23: DIV(s(X),n__s(Y)) -> GEQ(X,activate(Y))
24: DIV(s(X),n__s(Y)) -> DIV(minus(X,activate(Y)),n__s(activate(Y)))
25: DIV(s(X),n__s(Y)) -> MINUS(X,activate(Y))
26: DIV(s(X),n__s(Y)) -> ACTIVATE(Y)
27: IF(true,X,Y) -> ACTIVATE(X)
28: IF(false,X,Y) -> ACTIVATE(Y)
29: ACTIVATE(n__0) -> 0#
30: ACTIVATE(n__s(X)) -> S(X)

The approximated dependency graph contains 3 SCCs:
{19},
{16}
and {24}.

- Consider the SCC {19}.
The usable rules are {10-14}.
By taking the polynomial interpretation
[0] = [n__0] = 1,
[activate](x) = x,
[n__s](x) = [s](x) = x + 1
and [GEQ](x,y) = x + y + 1,
the rules in {10-14}
are weakly decreasing and
rule 19
is strictly decreasing.

- Consider the SCC {16}.
The usable rules are {10-14}.
By taking the polynomial interpretation
[0] = [n__0] = 1,
[activate](x) = x,
[n__s](x) = [s](x) = x + 1
and [MINUS](x,y) = x + y + 1,
the rules in {10-14}
are weakly decreasing and
rule 16
is strictly decreasing.

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

Hence the TRS is terminating.