Consider the TRS R consisting of the rewrite rules

1: minus_active(0,y) -> 0
2: mark(0) -> 0
3: minus_active(s(x),s(y)) -> minus_active(x,y)
4: mark(s(x)) -> s(mark(x))
5: ge_active(x,0) -> true
6: mark(minus(x,y)) -> minus_active(x,y)
7: ge_active(0,s(y)) -> false
8: mark(ge(x,y)) -> ge_active(x,y)
9: ge_active(s(x),s(y)) -> ge_active(x,y)
10: mark(div(x,y)) -> div_active(mark(x),y)
11: div_active(0,s(y)) -> 0
12: mark(if(x,y,z)) -> if_active(mark(x),y,z)
13: div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
14: if_active(true,x,y) -> mark(x)
15: minus_active(x,y) -> minus(x,y)
16: if_active(false,x,y) -> mark(y)
17: ge_active(x,y) -> ge(x,y)
18: if_active(x,y,z) -> if(x,y,z)
19: div_active(x,y) -> div(x,y)

There are 13 dependency pairs:

20: MINUS_ACTIVE(s(x),s(y)) -> MINUS_ACTIVE(x,y)
21: MARK(s(x)) -> MARK(x)
22: MARK(minus(x,y)) -> MINUS_ACTIVE(x,y)
23: MARK(ge(x,y)) -> GE_ACTIVE(x,y)
24: GE_ACTIVE(s(x),s(y)) -> GE_ACTIVE(x,y)
25: MARK(div(x,y)) -> DIV_ACTIVE(mark(x),y)
26: MARK(div(x,y)) -> MARK(x)
27: MARK(if(x,y,z)) -> IF_ACTIVE(mark(x),y,z)
28: MARK(if(x,y,z)) -> MARK(x)
29: DIV_ACTIVE(s(x),s(y)) -> IF_ACTIVE(ge_active(x,y),s(div(minus(x,y),s(y))),0)
30: DIV_ACTIVE(s(x),s(y)) -> GE_ACTIVE(x,y)
31: IF_ACTIVE(true,x,y) -> MARK(x)
32: IF_ACTIVE(false,x,y) -> MARK(y)

The approximated dependency graph contains 3 SCCs:
{24},
{20}
and {21,25-29,31,32}.

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

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

- Consider the SCC {21,25-29,31,32}.
By taking the polynomial interpretation
[0] = [false] = [ge](x,y) = [ge_active](x,y) = [true] = 0,
[mark](x) = [MARK](x) = [minus](x,y) = [minus_active](x,y) = x,
[s](x) = x + 1,
[div](x,y) = [div_active](x,y) = [DIV_ACTIVE](x,y) = x + y + 1
and [if](x,y,z) = [if_active](x,y,z) = [IF_ACTIVE](x,y,z) = x + y + z,
the rules in {1,2,4-10,12-19,25,27-29,31,32}
are weakly decreasing and
the rules in {3,11,21,26}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {25,27-29,31,32}.
By taking the polynomial interpretation
[0] = [false] = [ge](x,y) = [ge_active](x,y) = [true] = 0,
[s](x) = x,
[mark](x) = [MARK](x) = x + 1,
[minus](x,y) = [minus_active](x,y) = x + y + 1,
[if](x,y,z) = [if_active](x,y,z) = [IF_ACTIVE](x,y,z) = x + y + z + 1,
[div](x,y) = y
and [div_active](x,y) = [DIV_ACTIVE](x,y) = y + 1,
the rules in {3-5,7,9,10,12-18,25,27,29,31,32}
are weakly decreasing and
the rules in {1,2,6,8,11,19,28}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {25,27,29,31,32}.
By taking the polynomial interpretation
[0] = 0,
[false] = [true] = 1,
[s](x) = x,
[mark](x) = [MARK](x) = x + 1,
[ge](x,y) = [ge_active](x,y) = [minus](x,y) = [minus_active](x,y) = x + y + 1,
[div](x,y) = y,
[div_active](x,y) = [DIV_ACTIVE](x,y) = y + 1
and [if](x,y,z) = [if_active](x,y,z) = [IF_ACTIVE](x,y,z) = y + z + 1,
the rules in {3-5,7,9,10,13-18,25,29,31,32}
are weakly decreasing and
the rules in {1,2,6,8,11,12,19,27}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {25,29,31,32}.
By taking the polynomial interpretation
[0] = 0,
[false] = [ge](x,y) = [ge_active](x,y) = [minus](x,y) = [minus_active](x,y) = [s](x) = [true] = 1,
[mark](x) = [MARK](x) = x + 1,
[div](x,y) = [div_active](x,y) = [DIV_ACTIVE](x,y) = x + y + 1
and [if](x,y,z) = [if_active](x,y,z) = [IF_ACTIVE](x,y,z) = x + y + z + 1,
the rules in {3,5,7,9,10,12,13,15,17-19,25,29}
are weakly decreasing and
the rules in {1,2,4,6,8,11,14,16,31,32}
are strictly decreasing.




Hence the TRS is terminating.