### (0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
+(x, +(y, z)) → +(+(x, y), z)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))
not(true) → false
not(false) → true
and(x, true) → x
and(x, false) → false
if(true, x, y) → x
if(false, x, y) → y
ge(O(x), O(y)) → ge(x, y)
ge(O(x), I(y)) → not(ge(y, x))
ge(I(x), O(y)) → ge(x, y)
ge(I(x), I(y)) → ge(x, y)
ge(x, 0) → true
ge(0, O(x)) → ge(0, x)
ge(0, I(x)) → false
Log'(0) → 0
Log'(I(x)) → +(Log'(x), I(0))
Log'(O(x)) → if(ge(x, I(0)), +(Log'(x), I(0)), 0)
Log(x) → -(Log'(x), I(0))
Val(L(x)) → x
Val(N(x, l, r)) → x
Min(L(x)) → x
Min(N(x, l, r)) → Min(l)
Max(L(x)) → x
Max(N(x, l, r)) → Max(r)
BS(L(x)) → true
BS(N(x, l, r)) → and(and(ge(x, Max(l)), ge(Min(r), x)), and(BS(l), BS(r)))
Size(L(x)) → I(0)
Size(N(x, l, r)) → +(+(Size(l), Size(r)), I(1))
WB(L(x)) → true
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)))

Rewrite Strategy: INNERMOST

### (1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

### (2) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
-(z0, 0) → z0
-(0, z0) → 0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
not(true) → false
not(false) → true
and(z0, true) → z0
and(z0, false) → false
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
ge(z0, 0) → true
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
Log(z0) → -(Log'(z0), I(0))
Val(L(z0)) → z0
Val(N(z0, l, r)) → z0
Min(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
BS(L(z0)) → true
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
Size(L(z0)) → I(0)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
WB(L(z0)) → true
WB(N(z0, 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)))
Tuples:

O'(0) → c
+'(0, z0) → c1
+'(z0, 0) → c2
+'(O(z0), O(z1)) → c3(O'(+(z0, z1)), +'(z0, z1))
+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(I(z0), I(z1)) → c6(O'(+(+(z0, z1), I(0))), +'(+(z0, z1), I(0)), +'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(z0, 0) → c8
-'(0, z0) → c9
-'(O(z0), O(z1)) → c10(O'(-(z0, z1)), -'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(I(z0), I(z1)) → c13(O'(-(z0, z1)), -'(z0, z1))
NOT(true) → c14
NOT(false) → c15
AND(z0, true) → c16
AND(z0, false) → c17
IF(true, z0, z1) → c18
IF(false, z0, z1) → c19
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(O(z0), I(z1)) → c21(NOT(ge(z1, z0)), GE(z1, z0))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(z0, 0) → c24
GE(0, O(z0)) → c25(GE(0, z0))
GE(0, I(z0)) → c26
LOG'(0) → c27
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
LOG'(O(z0)) → c29(IF(ge(z0, I(0)), +(Log'(z0), I(0)), 0), GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0))
VAL(L(z0)) → c31
VAL(N(z0, l, r)) → c32
MIN(L(z0)) → c33
MIN(N(z0, l, r)) → c34(MIN(l))
MAX(L(z0)) → c35
MAX(N(z0, l, r)) → c36(MAX(r))
BS'(L(z0)) → c37
BS'(N(z0, l, r)) → c38(AND(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))), AND(ge(z0, Max(l)), ge(Min(r), z0)), GE(z0, Max(l)), MAX(l), GE(Min(r), z0), MIN(r), AND(BS(l), BS(r)), BS'(l), BS'(r))
SIZE(L(z0)) → c39
SIZE(N(z0, l, r)) → c40(+'(+(Size(l), Size(r)), I(1)), +'(Size(l), Size(r)), SIZE(l), SIZE(r))
WB'(L(z0)) → c41
WB'(N(z0, l, r)) → c42(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))), IF(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), GE(Size(l), Size(r)), SIZE(l), SIZE(r), GE(I(0), -(Size(l), Size(r))), -'(Size(l), Size(r)), SIZE(l), SIZE(r), GE(I(0), -(Size(r), Size(l))), -'(Size(r), Size(l)), SIZE(r), SIZE(l), AND(WB(l), WB(r)), WB'(l), WB'(r))
S tuples:

O'(0) → c
+'(0, z0) → c1
+'(z0, 0) → c2
+'(O(z0), O(z1)) → c3(O'(+(z0, z1)), +'(z0, z1))
+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(I(z0), I(z1)) → c6(O'(+(+(z0, z1), I(0))), +'(+(z0, z1), I(0)), +'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(z0, 0) → c8
-'(0, z0) → c9
-'(O(z0), O(z1)) → c10(O'(-(z0, z1)), -'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(I(z0), I(z1)) → c13(O'(-(z0, z1)), -'(z0, z1))
NOT(true) → c14
NOT(false) → c15
AND(z0, true) → c16
AND(z0, false) → c17
IF(true, z0, z1) → c18
IF(false, z0, z1) → c19
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(O(z0), I(z1)) → c21(NOT(ge(z1, z0)), GE(z1, z0))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(z0, 0) → c24
GE(0, O(z0)) → c25(GE(0, z0))
GE(0, I(z0)) → c26
LOG'(0) → c27
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
LOG'(O(z0)) → c29(IF(ge(z0, I(0)), +(Log'(z0), I(0)), 0), GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0))
VAL(L(z0)) → c31
VAL(N(z0, l, r)) → c32
MIN(L(z0)) → c33
MIN(N(z0, l, r)) → c34(MIN(l))
MAX(L(z0)) → c35
MAX(N(z0, l, r)) → c36(MAX(r))
BS'(L(z0)) → c37
BS'(N(z0, l, r)) → c38(AND(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))), AND(ge(z0, Max(l)), ge(Min(r), z0)), GE(z0, Max(l)), MAX(l), GE(Min(r), z0), MIN(r), AND(BS(l), BS(r)), BS'(l), BS'(r))
SIZE(L(z0)) → c39
SIZE(N(z0, l, r)) → c40(+'(+(Size(l), Size(r)), I(1)), +'(Size(l), Size(r)), SIZE(l), SIZE(r))
WB'(L(z0)) → c41
WB'(N(z0, l, r)) → c42(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))), IF(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), GE(Size(l), Size(r)), SIZE(l), SIZE(r), GE(I(0), -(Size(l), Size(r))), -'(Size(l), Size(r)), SIZE(l), SIZE(r), GE(I(0), -(Size(r), Size(l))), -'(Size(r), Size(l)), SIZE(r), SIZE(l), AND(WB(l), WB(r)), WB'(l), WB'(r))
K tuples:none
Defined Rule Symbols:

O, +, -, not, and, if, ge, Log', Log, Val, Min, Max, BS, Size, WB

Defined Pair Symbols:

O', +', -', NOT, AND, IF, GE, LOG', LOG, VAL, MIN, MAX, BS', SIZE, WB'

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42

### (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 26 trailing nodes:

AND(z0, false) → c17
NOT(false) → c15
MAX(L(z0)) → c35
-'(0, z0) → c9
IF(false, z0, z1) → c19
O'(0) → c
WB'(L(z0)) → c41
SIZE(N(z0, l, r)) → c40(+'(+(Size(l), Size(r)), I(1)), +'(Size(l), Size(r)), SIZE(l), SIZE(r))
AND(z0, true) → c16
BS'(L(z0)) → c37
BS'(N(z0, l, r)) → c38(AND(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))), AND(ge(z0, Max(l)), ge(Min(r), z0)), GE(z0, Max(l)), MAX(l), GE(Min(r), z0), MIN(r), AND(BS(l), BS(r)), BS'(l), BS'(r))
NOT(true) → c14
SIZE(L(z0)) → c39
MAX(N(z0, l, r)) → c36(MAX(r))
GE(z0, 0) → c24
+'(0, z0) → c1
VAL(N(z0, l, r)) → c32
IF(true, z0, z1) → c18
VAL(L(z0)) → c31
GE(0, I(z0)) → c26
MIN(N(z0, l, r)) → c34(MIN(l))
WB'(N(z0, l, r)) → c42(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))), IF(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), GE(Size(l), Size(r)), SIZE(l), SIZE(r), GE(I(0), -(Size(l), Size(r))), -'(Size(l), Size(r)), SIZE(l), SIZE(r), GE(I(0), -(Size(r), Size(l))), -'(Size(r), Size(l)), SIZE(r), SIZE(l), AND(WB(l), WB(r)), WB'(l), WB'(r))
+'(z0, 0) → c2
LOG'(0) → c27
MIN(L(z0)) → c33
-'(z0, 0) → c8

### (4) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
-(z0, 0) → z0
-(0, z0) → 0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
not(true) → false
not(false) → true
and(z0, true) → z0
and(z0, false) → false
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
ge(z0, 0) → true
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
Log(z0) → -(Log'(z0), I(0))
Val(L(z0)) → z0
Val(N(z0, l, r)) → z0
Min(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
BS(L(z0)) → true
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
Size(L(z0)) → I(0)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
WB(L(z0)) → true
WB(N(z0, 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)))
Tuples:

+'(O(z0), O(z1)) → c3(O'(+(z0, z1)), +'(z0, z1))
+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(I(z0), I(z1)) → c6(O'(+(+(z0, z1), I(0))), +'(+(z0, z1), I(0)), +'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), O(z1)) → c10(O'(-(z0, z1)), -'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(I(z0), I(z1)) → c13(O'(-(z0, z1)), -'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(O(z0), I(z1)) → c21(NOT(ge(z1, z0)), GE(z1, z0))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
LOG'(O(z0)) → c29(IF(ge(z0, I(0)), +(Log'(z0), I(0)), 0), GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0))
S tuples:

+'(O(z0), O(z1)) → c3(O'(+(z0, z1)), +'(z0, z1))
+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(I(z0), I(z1)) → c6(O'(+(+(z0, z1), I(0))), +'(+(z0, z1), I(0)), +'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), O(z1)) → c10(O'(-(z0, z1)), -'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(I(z0), I(z1)) → c13(O'(-(z0, z1)), -'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(O(z0), I(z1)) → c21(NOT(ge(z1, z0)), GE(z1, z0))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
LOG'(O(z0)) → c29(IF(ge(z0, I(0)), +(Log'(z0), I(0)), 0), GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0))
K tuples:none
Defined Rule Symbols:

O, +, -, not, and, if, ge, Log', Log, Val, Min, Max, BS, Size, WB

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c3, c4, c5, c6, c7, c10, c11, c12, c13, c20, c21, c22, c23, c25, c28, c29, c30

### (5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 6 trailing tuple parts

### (6) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
-(z0, 0) → z0
-(0, z0) → 0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
not(true) → false
not(false) → true
and(z0, true) → z0
and(z0, false) → false
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
ge(z0, 0) → true
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
Log(z0) → -(Log'(z0), I(0))
Val(L(z0)) → z0
Val(N(z0, l, r)) → z0
Min(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
BS(L(z0)) → true
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
Size(L(z0)) → I(0)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
WB(L(z0)) → true
WB(N(z0, 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)))
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
K tuples:none
Defined Rule Symbols:

O, +, -, not, and, if, ge, Log', Log, Val, Min, Max, BS, Size, WB

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c30, c3, c6, c10, c13, c21, c29

### (7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

### (8) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
-(z0, 0) → z0
-(0, z0) → 0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
not(true) → false
not(false) → true
and(z0, true) → z0
and(z0, false) → false
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
ge(z0, 0) → true
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
Log(z0) → -(Log'(z0), I(0))
Val(L(z0)) → z0
Val(N(z0, l, r)) → z0
Min(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
BS(L(z0)) → true
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
Size(L(z0)) → I(0)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
WB(L(z0)) → true
WB(N(z0, 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)))
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
LOG(z0) → c(LOG'(z0))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
LOG(z0) → c(LOG'(z0))
K tuples:none
Defined Rule Symbols:

O, +, -, not, and, if, ge, Log', Log, Val, Min, Max, BS, Size, WB

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

LOG(z0) → c(LOG'(z0))

### (10) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
-(z0, 0) → z0
-(0, z0) → 0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
not(true) → false
not(false) → true
and(z0, true) → z0
and(z0, false) → false
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
ge(z0, 0) → true
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
Log(z0) → -(Log'(z0), I(0))
Val(L(z0)) → z0
Val(N(z0, l, r)) → z0
Min(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
BS(L(z0)) → true
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
Size(L(z0)) → I(0)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
WB(L(z0)) → true
WB(N(z0, 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)))
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
K tuples:none
Defined Rule Symbols:

O, +, -, not, and, if, ge, Log', Log, Val, Min, Max, BS, Size, WB

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

LOG(z0) → c(-'(Log'(z0), I(0)))

### (12) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
-(z0, 0) → z0
-(0, z0) → 0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
not(true) → false
not(false) → true
and(z0, true) → z0
and(z0, false) → false
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
ge(z0, 0) → true
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
Log(z0) → -(Log'(z0), I(0))
Val(L(z0)) → z0
Val(N(z0, l, r)) → z0
Min(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
BS(L(z0)) → true
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
Size(L(z0)) → I(0)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
WB(L(z0)) → true
WB(N(z0, 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)))
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
Defined Rule Symbols:

O, +, -, not, and, if, ge, Log', Log, Val, Min, Max, BS, Size, WB

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (13) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

and(z0, true) → z0
and(z0, false) → false
Log(z0) → -(Log'(z0), I(0))
Val(L(z0)) → z0
Val(N(z0, l, r)) → z0
Min(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
BS(L(z0)) → true
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
Size(L(z0)) → I(0)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
WB(L(z0)) → true
WB(N(z0, 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)))

### (14) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (15) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [3] + x1 + x2
POL(+'(x1, x2)) = [4]x2
POL(-(x1, x2)) = [4] + [4]x2
POL(-'(x1, x2)) = 0
POL(0) = 0
POL(1) = [2]
POL(GE(x1, x2)) = 0
POL(I(x1)) = x1
POL(LOG(x1)) = [5]x1
POL(LOG'(x1)) = 0
POL(Log'(x1)) = [1] + [3]x1
POL(O(x1)) = [4] + x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = [2]
POL(ge(x1, x2)) = [2] + [3]x1
POL(if(x1, x2, x3)) = [2] + [2]x1 + [3]x2 + [2]x3
POL(not(x1)) = [4] + [2]x1
POL(true) = [5]

### (16) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (17) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
We considered the (Usable) Rules:none
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [3]
POL(+'(x1, x2)) = 0
POL(-(x1, x2)) = [2] + [2]x2
POL(-'(x1, x2)) = 0
POL(0) = [4]
POL(1) = [2]
POL(GE(x1, x2)) = [1]
POL(I(x1)) = x1
POL(LOG(x1)) = [3]x1
POL(LOG'(x1)) = x1
POL(Log'(x1)) = [4] + [5]x1
POL(O(x1)) = [2] + [2]x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = [4]
POL(ge(x1, x2)) = [4]x1
POL(if(x1, x2, x3)) = [2] + [3]x1 + [2]x2 + [2]x3
POL(not(x1)) = [2]x1
POL(true) = [2]

### (18) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (19) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
We considered the (Usable) Rules:none
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [3] + [5]x2
POL(+'(x1, x2)) = 0
POL(-(x1, x2)) = [5] + [5]x2
POL(-'(x1, x2)) = 0
POL(0) = 0
POL(1) = [3]
POL(GE(x1, x2)) = [1] + [3]x1 + [5]x2
POL(I(x1)) = x1
POL(LOG(x1)) = [5] + [2]x1
POL(LOG'(x1)) = [4]x1
POL(Log'(x1)) = [5]
POL(O(x1)) = [1] + [2]x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = 0
POL(ge(x1, x2)) = [2] + [2]x1 + [2]x2
POL(if(x1, x2, x3)) = [3] + [3]x1 + [2]x2 + [4]x3
POL(not(x1)) = [3] + [2]x1
POL(true) = [4]

### (20) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (21) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
We considered the (Usable) Rules:none
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [2] + [5]x2
POL(+'(x1, x2)) = 0
POL(-(x1, x2)) = [5] + x1 + [5]x2
POL(-'(x1, x2)) = 0
POL(0) = 0
POL(1) = [3]
POL(GE(x1, x2)) = [1]
POL(I(x1)) = [4] + x1
POL(LOG(x1)) = [5] + [3]x1
POL(LOG'(x1)) = x1
POL(Log'(x1)) = [3]x1
POL(O(x1)) = [1] + [4]x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = [2]
POL(ge(x1, x2)) = [4] + [3]x1 + [4]x2
POL(if(x1, x2, x3)) = [2]x1 + [2]x2 + [4]x3
POL(not(x1)) = [2] + [2]x1
POL(true) = [2]

### (22) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (23) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

GE(I(z0), I(z1)) → c23(GE(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [3]
POL(+'(x1, x2)) = 0
POL(-(x1, x2)) = [5] + [2]x1
POL(-'(x1, x2)) = 0
POL(0) = 0
POL(1) = [4]
POL(GE(x1, x2)) = [4]x1 + [4]x2
POL(I(x1)) = [4] + x1
POL(LOG(x1)) = [2] + [5]x1
POL(LOG'(x1)) = [4]x1
POL(Log'(x1)) = [5]x1
POL(O(x1)) = [4] + [4]x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = 0
POL(ge(x1, x2)) = [2] + [3]x1 + [4]x2
POL(if(x1, x2, x3)) = [4]x2 + [2]x3
POL(not(x1)) = 0
POL(true) = [5]

### (24) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (25) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [2]
POL(+'(x1, x2)) = 0
POL(-(x1, x2)) = [3] + [3]x2
POL(-'(x1, x2)) = x2
POL(0) = [4]
POL(1) = 0
POL(GE(x1, x2)) = 0
POL(I(x1)) = x1
POL(LOG(x1)) = [5]
POL(LOG'(x1)) = 0
POL(Log'(x1)) = [5] + x1
POL(O(x1)) = [1] + [2]x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = [2]
POL(ge(x1, x2)) = [1] + [2]x1 + [4]x2
POL(if(x1, x2, x3)) = [4] + [2]x1 + [4]x2 + [2]x3
POL(not(x1)) = [2] + [2]x1
POL(true) = 0

### (26) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (27) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

-'(I(z0), I(z1)) → c13(-'(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [1]
POL(+'(x1, x2)) = 0
POL(-(x1, x2)) = [2]
POL(-'(x1, x2)) = x2
POL(0) = [1]
POL(1) = 0
POL(GE(x1, x2)) = 0
POL(I(x1)) = [1] + x1
POL(LOG(x1)) = [3] + [5]x1
POL(LOG'(x1)) = 0
POL(Log'(x1)) = [1] + [2]x1
POL(O(x1)) = [4] + x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = 0
POL(ge(x1, x2)) = [5]x1 + [2]x2
POL(if(x1, x2, x3)) = [1] + x2 + [4]x3
POL(not(x1)) = [5] + [2]x1
POL(true) = [3]

### (28) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (29) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

+'(O(z0), I(z1)) → c4(+'(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [2]x1 + [2]x2
POL(+'(x1, x2)) = x2
POL(-(x1, x2)) = [3] + x1 + [2]x2
POL(-'(x1, x2)) = 0
POL(0) = 0
POL(1) = [2]
POL(GE(x1, x2)) = x1 + [4]x2
POL(I(x1)) = [1] + x1
POL(LOG(x1)) = [3] + [3]x1
POL(LOG'(x1)) = [2]x1
POL(Log'(x1)) = [3] + [3]x1
POL(O(x1)) = [3] + [4]x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = [2]
POL(ge(x1, x2)) = [4] + [2]x1 + [2]x2
POL(if(x1, x2, x3)) = [2] + [5]x1 + [4]x2 + [4]x3
POL(not(x1)) = [2] + [2]x1
POL(true) = [3]

### (30) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
+'(O(z0), I(z1)) → c4(+'(z0, z1))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (31) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
We considered the (Usable) Rules:

if(false, z0, z1) → z1
O(0) → 0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
Log'(0) → 0
if(true, z0, z1) → z0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(z0, 0) → z0
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
Log'(I(z0)) → +(Log'(z0), I(0))
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = x1 + [2]x2
POL(+'(x1, x2)) = [2]x22 + x1·x2
POL(-(x1, x2)) = 0
POL(-'(x1, x2)) = 0
POL(0) = 0
POL(1) = 0
POL(GE(x1, x2)) = [2]x1·x2
POL(I(x1)) = [1] + x1
POL(LOG(x1)) = [1] + [2]x12
POL(LOG'(x1)) = [2]x1 + [2]x12
POL(Log'(x1)) = [2]x1
POL(O(x1)) = [1] + x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(if(x1, x2, x3)) = x2 + [2]x3
POL(not(x1)) = 0
POL(true) = 0

### (32) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:

-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (33) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
We considered the (Usable) Rules:

if(false, z0, z1) → z1
O(0) → 0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
Log'(0) → 0
if(true, z0, z1) → z0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
-(z0, 0) → z0
-(I(z0), O(z1)) → I(-(z0, z1))
+(z0, 0) → z0
+(0, z0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
-(0, z0) → 0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
Log'(I(z0)) → +(Log'(z0), I(0))
And the Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = x1 + x2
POL(+'(x1, x2)) = 0
POL(-(x1, x2)) = x1 + x2
POL(-'(x1, x2)) = x1·x2
POL(0) = 0
POL(1) = 0
POL(GE(x1, x2)) = [2]x2 + [3]x1·x2
POL(I(x1)) = [1] + x1
POL(LOG(x1)) = [3] + [2]x1
POL(LOG'(x1)) = [2]x12
POL(Log'(x1)) = x1
POL(O(x1)) = [1] + x1
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c13(x1)) = x1
POL(c20(x1)) = x1
POL(c21(x1)) = x1
POL(c22(x1)) = x1
POL(c23(x1)) = x1
POL(c25(x1)) = x1
POL(c28(x1, x2)) = x1 + x2
POL(c29(x1, x2, x3)) = x1 + x2 + x3
POL(c3(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(if(x1, x2, x3)) = x2 + [2]x3
POL(not(x1)) = 0
POL(true) = 0

### (34) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
O(0) → 0
-(z0, 0) → z0
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(I(z0), O(z1)) → I(-(z0, z1))
-(I(z0), I(z1)) → O(-(z0, z1))
-(0, z0) → 0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), I(z1)) → ge(z0, z1)
ge(O(z0), O(z1)) → ge(z0, z1)
ge(I(z0), O(z1)) → ge(z0, z1)
ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
not(true) → false
not(false) → true
Tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
LOG(z0) → c(-'(Log'(z0), I(0)))
S tuples:none
K tuples:

LOG(z0) → c(-'(Log'(z0), I(0)))
+'(I(z0), O(z1)) → c5(+'(z0, z1))
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c3(+'(z0, z1))
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), O(z1)) → c20(GE(z0, z1))
GE(I(z0), O(z1)) → c22(GE(z0, z1))
GE(0, O(z0)) → c25(GE(0, z0))
GE(O(z0), I(z1)) → c21(GE(z1, z0))
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))
GE(I(z0), I(z1)) → c23(GE(z0, z1))
-'(I(z0), O(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c13(-'(z0, z1))
+'(O(z0), I(z1)) → c4(+'(z0, z1))
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1))
Defined Rule Symbols:

+, O, -, Log', if, ge, not

Defined Pair Symbols:

+', -', GE, LOG', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c

### (35) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty