Consider the TRS R consisting of the rewrite rules

1: O(0) -> 0
2: 0 + x -> x
3: x + 0 -> x
4: O(x) + O(y) -> O(x + y)
5: O(x) + I(y) -> I(x + y)
6: I(x) + O(y) -> I(x + y)
7: I(x) + I(y) -> O((x + y) + I(0))
8: x + (y + z) -> (x + y) + z
9: x - 0 -> x
10: 0 - x -> 0
11: O(x) - O(y) -> O(x - y)
12: O(x) - I(y) -> I((x - y) - I(1))
13: I(x) - O(y) -> I(x - y)
14: I(x) - I(y) -> O(x - y)
15: not(true) -> false
16: not(false) -> true
17: and(x,true) -> x
18: and(x,false) -> false
19: if(true,x,y) -> x
20: if(false,x,y) -> y
21: ge(O(x),O(y)) -> ge(x,y)
22: ge(O(x),I(y)) -> not(ge(y,x))
23: ge(I(x),O(y)) -> ge(x,y)
24: ge(I(x),I(y)) -> ge(x,y)
25: ge(x,0) -> true
26: ge(0,O(x)) -> ge(0,x)
27: ge(0,I(x)) -> false
28: Log'(0) -> 0
29: Log'(I(x)) -> Log'(x) + I(0)
30: Log'(O(x)) -> if(ge(x,I(0)),Log'(x) + I(0),0)
31: Log(x) -> Log'(x) - I(0)
32: Val(L(x)) -> x
33: Val(N(x,l,r)) -> x
34: Min(L(x)) -> x
35: Min(N(x,l,r)) -> Min(l)
36: Max(L(x)) -> x
37: Max(N(x,l,r)) -> Max(r)
38: BS(L(x)) -> true
39: BS(N(x,l,r)) -> and(and(ge(x,Max(l)),ge(Min(r),x)),and(BS(l),BS(r)))
40: Size(L(x)) -> I(0)
41: Size(N(x,l,r)) -> (Size(l) + Size(r)) + I(1)
42: WB(L(x)) -> true
43: WB(N(x,l,r)) -> and(if(ge(Size(l),Size(r)),ge(I(0),Size(l) - Size(r)),ge(I(0),Size(r) - Size(l))),and(WB(l),WB(r)))

There are 57 dependency pairs:

44: O(x) +# O(y) -> O#(x + y)
45: O(x) +# O(y) -> x +# y
46: O(x) +# I(y) -> x +# y
47: I(x) +# O(y) -> x +# y
48: I(x) +# I(y) -> O#((x + y) + I(0))
49: I(x) +# I(y) -> (x + y) +# I(0)
50: I(x) +# I(y) -> x +# y
51: x +# (y + z) -> (x + y) +# z
52: x +# (y + z) -> x +# y
53: O(x) -# O(y) -> O#(x - y)
54: O(x) -# O(y) -> x -# y
55: O(x) -# I(y) -> (x - y) -# I(1)
56: O(x) -# I(y) -> x -# y
57: I(x) -# O(y) -> x -# y
58: I(x) -# I(y) -> O#(x - y)
59: I(x) -# I(y) -> x -# y
60: GE(O(x),O(y)) -> GE(x,y)
61: GE(O(x),I(y)) -> NOT(ge(y,x))
62: GE(O(x),I(y)) -> GE(y,x)
63: GE(I(x),O(y)) -> GE(x,y)
64: GE(I(x),I(y)) -> GE(x,y)
65: GE(0,O(x)) -> GE(0,x)
66: Log'#(I(x)) -> Log'(x) +# I(0)
67: Log'#(I(x)) -> Log'#(x)
68: Log'#(O(x)) -> IF(ge(x,I(0)),Log'(x) + I(0),0)
69: Log'#(O(x)) -> GE(x,I(0))
70: Log'#(O(x)) -> Log'(x) +# I(0)
71: Log'#(O(x)) -> Log'#(x)
72: Log#(x) -> Log'(x) -# I(0)
73: Log#(x) -> Log'#(x)
74: Min#(N(x,l,r)) -> Min#(l)
75: Max#(N(x,l,r)) -> Max#(r)
76: BS#(N(x,l,r)) -> AND(and(ge(x,Max(l)),ge(Min(r),x)),and(BS(l),BS(r)))
77: BS#(N(x,l,r)) -> AND(ge(x,Max(l)),ge(Min(r),x))
78: BS#(N(x,l,r)) -> GE(x,Max(l))
79: BS#(N(x,l,r)) -> Max#(l)
80: BS#(N(x,l,r)) -> GE(Min(r),x)
81: BS#(N(x,l,r)) -> Min#(r)
82: BS#(N(x,l,r)) -> AND(BS(l),BS(r))
83: BS#(N(x,l,r)) -> BS#(l)
84: BS#(N(x,l,r)) -> BS#(r)
85: Size#(N(x,l,r)) -> (Size(l) + Size(r)) +# I(1)
86: Size#(N(x,l,r)) -> Size(l) +# Size(r)
87: Size#(N(x,l,r)) -> Size#(l)
88: Size#(N(x,l,r)) -> Size#(r)
89: WB#(N(x,l,r)) -> AND(if(ge(Size(l),Size(r)),ge(I(0),Size(l) - Size(r)),ge(I(0),Size(r) - Size(l))),and(WB(l),WB(r)))
90: WB#(N(x,l,r)) -> IF(ge(Size(l),Size(r)),ge(I(0),Size(l) - Size(r)),ge(I(0),Size(r) - Size(l)))
91: WB#(N(x,l,r)) -> GE(Size(l),Size(r))
92: WB#(N(x,l,r)) -> GE(I(0),Size(l) - Size(r))
93: WB#(N(x,l,r)) -> Size(l) -# Size(r)
94: WB#(N(x,l,r)) -> GE(I(0),Size(r) - Size(l))
95: WB#(N(x,l,r)) -> Size(r) -# Size(l)
96: WB#(N(x,l,r)) -> Size#(r)
97: WB#(N(x,l,r)) -> Size#(l)
98: WB#(N(x,l,r)) -> AND(WB(l),WB(r))
99: WB#(N(x,l,r)) -> WB#(l)
100: WB#(N(x,l,r)) -> WB#(r)

The approximated dependency graph contains 5 SCCs:
{65},
{45-47,49-52},
{54-57,59},
{60,62-64}
and {67,71}.

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

- Consider the SCC {45-47,49-52}.
The usable rules are {1-8}.
By taking the polynomial interpretation
[0] = 1,
[O](x) = x,
[I](x) = x + 1,
[+](x,y) = x + y
and [+#](x,y) = x + y + 1,
the rules in {1,4-8,45,49,51,52}
are weakly decreasing and
the rules in {2,3,46,47,50}
are strictly decreasing.
There are 2 new SCCs.

- Consider the SCC {49}.
By taking the polynomial interpretation
[0] = 0,
[I](x) = [O](x) = x + 1,
[+](x,y) = x + y
and [+#](x,y) = x + y + 1,
the rules in {2,3,7,8}
are weakly decreasing and
the rules in {1,4-6,49}
are strictly decreasing.

- Consider the SCC {45,51,52}.
By taking the polynomial interpretation
[0] = 0,
[O](x) = x,
[I](x) = x + 1
and [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {1,4-8,45,51}
are weakly decreasing and
the rules in {2,3,52}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {45,51}.
By taking the polynomial interpretation
[0] = 0,
[O](x) = x,
[I](x) = x + 1,
[+](x,y) = x + y + 1
and [+#](x,y) = y + 1,
the rules in {1,4-8,45}
are weakly decreasing and
the rules in {2,3,51}
are strictly decreasing.
There is one new SCC.

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




- Consider the SCC {54-57,59}.
The usable rules are {1,9-14}.
By taking the polynomial interpretation
[1] = 0,
[0] = 1,
[I](x) = [O](x) = x + 1,
[-](x,y) = x + y
and [-#](x,y) = x + y + 1,
the rules in {10,12}
are weakly decreasing and
the rules in {1,9,11,13,14,54-57,59}
are strictly decreasing.

- Consider the SCC {60,62-64}.
There are no usable rules.
By taking the polynomial interpretation
[I](x) = [O](x) = x + 1
and [GE](x,y) = x + y + 1,
the rules in {60,62-64}
are strictly decreasing.

- Consider the SCC {67,71}.
There are no usable rules.
By taking the polynomial interpretation
[I](x) = [Log'#](x) = [O](x) = x + 1,
the rules in {67,71}
are strictly decreasing.

Hence the TRS is terminating.