Consider the TRS R consisting of the rewrite rules

1: a__minus(0,Y) -> 0
2: a__minus(s(X),s(Y)) -> a__minus(X,Y)
3: a__geq(X,0) -> true
4: a__geq(0,s(Y)) -> false
5: a__geq(s(X),s(Y)) -> a__geq(X,Y)
6: a__div(0,s(Y)) -> 0
7: a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0)
8: a__if(true,X,Y) -> mark(X)
9: a__if(false,X,Y) -> mark(Y)
10: mark(minus(X1,X2)) -> a__minus(X1,X2)
11: mark(geq(X1,X2)) -> a__geq(X1,X2)
12: mark(div(X1,X2)) -> a__div(mark(X1),X2)
13: mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
14: mark(0) -> 0
15: mark(s(X)) -> s(mark(X))
16: mark(true) -> true
17: mark(false) -> false
18: a__minus(X1,X2) -> minus(X1,X2)
19: a__geq(X1,X2) -> geq(X1,X2)
20: a__div(X1,X2) -> div(X1,X2)
21: a__if(X1,X2,X3) -> if(X1,X2,X3)

There are 13 dependency pairs:

22: A__MINUS(s(X),s(Y)) -> A__MINUS(X,Y)
23: A__GEQ(s(X),s(Y)) -> A__GEQ(X,Y)
24: A__DIV(s(X),s(Y)) -> A__IF(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0)
25: A__DIV(s(X),s(Y)) -> A__GEQ(X,Y)
26: A__IF(true,X,Y) -> MARK(X)
27: A__IF(false,X,Y) -> MARK(Y)
28: MARK(minus(X1,X2)) -> A__MINUS(X1,X2)
29: MARK(geq(X1,X2)) -> A__GEQ(X1,X2)
30: MARK(div(X1,X2)) -> A__DIV(mark(X1),X2)
31: MARK(div(X1,X2)) -> MARK(X1)
32: MARK(if(X1,X2,X3)) -> A__IF(mark(X1),X2,X3)
33: MARK(if(X1,X2,X3)) -> MARK(X1)
34: MARK(s(X)) -> MARK(X)

The approximated dependency graph contains 3 SCCs:
{23},
{22}
and {24,26,27,30-34}.

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

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

- Consider the SCC {24,26,27,30-34}.
By taking the polynomial interpretation
[0] = [a__geq](x,y) = [false] = [geq](x,y) = [true] = 0,
[a__minus](x,y) = [mark](x) = [MARK](x) = [minus](x,y) = x,
[s](x) = x + 1,
[a__div](x,y) = [A__DIV](x,y) = [div](x,y) = x + y + 1
and [a__if](x,y,z) = [A__IF](x,y,z) = [if](x,y,z) = x + y + z,
the rules in {1,3-5,7-21,24,26,27,30,32,33}
are weakly decreasing and
the rules in {2,6,31,34}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {24,26,27,30,32,33}.
By taking the polynomial interpretation
[0] = [a__geq](x,y) = [false] = [geq](x,y) = [true] = 0,
[s](x) = x,
[mark](x) = [MARK](x) = x + 1,
[a__minus](x,y) = [minus](x,y) = x + y + 1,
[a__if](x,y,z) = [A__IF](x,y,z) = [if](x,y,z) = x + y + z + 1,
[div](x,y) = y
and [a__div](x,y) = [A__DIV](x,y) = y + 1,
the rules in {2-5,7-9,12,13,15,18,19,21,24,26,27,30,32}
are weakly decreasing and
the rules in {1,6,10,11,14,16,17,20,33}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {24,26,27,30,32}.
By taking the polynomial interpretation
[0] = 0,
[false] = [true] = 1,
[s](x) = x,
[mark](x) = [MARK](x) = x + 1,
[a__geq](x,y) = [a__minus](x,y) = [geq](x,y) = [minus](x,y) = x + y + 1,
[div](x,y) = y,
[a__div](x,y) = [A__DIV](x,y) = y + 1
and [a__if](x,y,z) = [A__IF](x,y,z) = [if](x,y,z) = y + z + 1,
the rules in {2-5,7-9,12,15,18,19,21,24,26,27,30}
are weakly decreasing and
the rules in {1,6,10,11,13,14,16,17,20,32}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {24,26,27,30}.
By taking the polynomial interpretation
[0] = [a__geq](x,y) = [a__minus](x,y) = [false] = [geq](x,y) = [minus](x,y) = [s](x) = [true] = 1,
[mark](x) = x,
[MARK](x) = x + 1,
[a__div](x,y) = [A__DIV](x,y) = [div](x,y) = x + y + 1,
[a__if](x,y,z) = [if](x,y,z) = x + y + z
and [A__IF](x,y,z) = y + z + 1,
the rules in {1-5,7,10-21,24,26,27}
are weakly decreasing and
the rules in {6,8,9,30}
are strictly decreasing.




Hence the TRS is terminating.