44.60/12.64 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

44.60/12.64

44.60/12.64
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS

44.60/12.64

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

44.60/12.64

↳2 CdtProblem

44.60/12.64

↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

44.60/12.64

↳4 CdtProblem

44.60/12.64

↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))

44.60/12.64

↳6 CdtProblem

44.60/12.64

↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)

44.60/12.64

↳8 CdtProblem

44.60/12.64

↳9 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

44.60/12.64

↳10 CdtProblem

44.60/12.64

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

44.60/12.64

↳12 CdtProblem

44.60/12.64

↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

44.60/12.64

↳14 CdtProblem

44.60/12.64

↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

44.60/12.64

↳16 CdtProblem

44.60/12.64

↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

44.60/12.64

↳18 CdtProblem

44.60/12.64

↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

44.60/12.64

↳20 CdtProblem

44.60/12.64

↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

44.60/12.64

↳22 CdtProblem

44.60/12.64

↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

44.60/12.64

↳24 CdtProblem

44.60/12.64

↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

44.60/12.64

↳26 CdtProblem

44.60/12.64

↳27 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

44.60/12.64

↳28 CdtProblem

44.60/12.64

↳29 SIsEmptyProof (BOTH BOUNDS(ID, ID))

44.60/12.64

↳30 BOUNDS(O(1), O(1))

44.60/12.64

44.60/12.64 44.60/12.64

44.60/12.64

(0) Obligation:

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

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

44.60/12.64

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

Converted CpxTRS to CDT

44.60/12.64

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.64
+(0, z0) → z0 44.60/12.64
+(z0, 0) → z0 44.60/12.64
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.64
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.64
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.64
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.64
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.64
-(z0, 0) → z0 44.60/12.64
-(0, z0) → 0 44.60/12.64
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.64
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.64
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.64
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.64
not(true) → false 44.60/12.64
not(false) → true 44.60/12.64
and(z0, true) → z0 44.60/12.64
and(z0, false) → false 44.60/12.64
if(true, z0, z1) → z0 44.60/12.64
if(false, z0, z1) → z1 44.60/12.64
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.64
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.64
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.64
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.64
ge(z0, 0) → true 44.60/12.64
ge(0, O(z0)) → ge(0, z0) 44.60/12.64
ge(0, I(z0)) → false 44.60/12.64
Log'(0) → 0 44.60/12.64
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.64
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.64
Log(z0) → -(Log'(z0), I(0)) 44.60/12.64
Val(L(z0)) → z0 44.60/12.64
Val(N(z0, l, r)) → z0 44.60/12.64
Min(L(z0)) → z0 44.60/12.64
Min(N(z0, l, r)) → Min(l) 44.60/12.64
Max(L(z0)) → z0 44.60/12.64
Max(N(z0, l, r)) → Max(r) 44.60/12.64
BS(L(z0)) → true 44.60/12.64
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.64
Size(L(z0)) → I(0) 44.60/12.64
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.64
WB(L(z0)) → true 44.60/12.64
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)) 44.60/12.64
+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.64
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.64
+'(I(z0), I(z1)) → c6(O'(+(+(z0, z1), I(0))), +'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.64
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.64
-'(O(z0), O(z1)) → c10(O'(-(z0, z1)), -'(z0, z1)) 44.60/12.64
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.64
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.64
-'(I(z0), I(z1)) → c13(O'(-(z0, z1)), -'(z0, z1)) 44.60/12.64
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.64
GE(O(z0), I(z1)) → c21(NOT(ge(z1, z0)), GE(z1, z0)) 44.60/12.64
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.64
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.64
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.64
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.64
LOG'(O(z0)) → c29(IF(ge(z0, I(0)), +(Log'(z0), I(0)), 0), GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.64
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.64
MIN(N(z0, l, r)) → c34(MIN(l)) 44.60/12.64
MAX(N(z0, l, r)) → c36(MAX(r)) 44.60/12.64
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)) 44.60/12.64
SIZE(N(z0, l, r)) → c40(+'(+(Size(l), Size(r)), I(1)), +'(Size(l), Size(r)), SIZE(l), SIZE(r)) 44.60/12.64
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(z0), O(z1)) → c3(O'(+(z0, z1)), +'(z0, z1)) 44.60/12.64
+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.64
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.64
+'(I(z0), I(z1)) → c6(O'(+(+(z0, z1), I(0))), +'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.64
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.64
-'(O(z0), O(z1)) → c10(O'(-(z0, z1)), -'(z0, z1)) 44.60/12.64
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.64
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.64
-'(I(z0), I(z1)) → c13(O'(-(z0, z1)), -'(z0, z1)) 44.60/12.64
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.64
GE(O(z0), I(z1)) → c21(NOT(ge(z1, z0)), GE(z1, z0)) 44.60/12.64
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.64
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.64
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.64
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.64
LOG'(O(z0)) → c29(IF(ge(z0, I(0)), +(Log'(z0), I(0)), 0), GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.64
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.64
MIN(N(z0, l, r)) → c34(MIN(l)) 44.60/12.64
MAX(N(z0, l, r)) → c36(MAX(r)) 44.60/12.64
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)) 44.60/12.64
SIZE(N(z0, l, r)) → c40(+'(+(Size(l), Size(r)), I(1)), +'(Size(l), Size(r)), SIZE(l), SIZE(r)) 44.60/12.64
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:

+', -', GE, LOG', LOG, MIN, MAX, BS', SIZE, WB'

Compound Symbols:

c3, c4, c5, c6, c7, c10, c11, c12, c13, c20, c21, c22, c23, c25, c28, c29, c30, c34, c36, c38, c40, c42

44.60/12.64

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 37 trailing tuple parts

44.60/12.64

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.64
+(0, z0) → z0 44.60/12.64
+(z0, 0) → z0 44.60/12.64
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.64
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.64
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.64
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.64
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.64
-(z0, 0) → z0 44.60/12.64
-(0, z0) → 0 44.60/12.64
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.64
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.64
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.64
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.64
not(true) → false 44.60/12.64
not(false) → true 44.60/12.64
and(z0, true) → z0 44.60/12.64
and(z0, false) → false 44.60/12.64
if(true, z0, z1) → z0 44.60/12.64
if(false, z0, z1) → z1 44.60/12.64
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.64
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.64
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.64
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.64
ge(z0, 0) → true 44.60/12.64
ge(0, O(z0)) → ge(0, z0) 44.60/12.64
ge(0, I(z0)) → false 44.60/12.64
Log'(0) → 0 44.60/12.64
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.64
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.64
Log(z0) → -(Log'(z0), I(0)) 44.60/12.64
Val(L(z0)) → z0 44.60/12.64
Val(N(z0, l, r)) → z0 44.60/12.64
Min(L(z0)) → z0 44.60/12.64
Min(N(z0, l, r)) → Min(l) 44.60/12.64
Max(L(z0)) → z0 44.60/12.64
Max(N(z0, l, r)) → Max(r) 44.60/12.64
BS(L(z0)) → true 44.60/12.64
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.66
Size(L(z0)) → I(0) 44.60/12.66
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.66
WB(L(z0)) → true 44.60/12.66
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)) 44.60/12.66
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.66
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.66
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.66
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.66
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.66
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.66
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.66
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.66
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.66
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.66
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.66
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.66
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.66
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
MIN(N(z0, l, r)) → c34 44.60/12.66
MAX(N(z0, l, r)) → c36 44.60/12.66
BS'(N(z0, l, r)) → c38 44.60/12.66
SIZE(N(z0, l, r)) → c40 44.60/12.66
WB'(N(z0, l, r)) → c42

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.66
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.66
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.66
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.66
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.66
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.66
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.66
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.66
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.66
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
LOG(z0) → c30(-'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.66
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.66
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.66
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.66
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.66
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
MIN(N(z0, l, r)) → c34 44.60/12.66
MAX(N(z0, l, r)) → c36 44.60/12.66
BS'(N(z0, l, r)) → c38 44.60/12.66
SIZE(N(z0, l, r)) → c40 44.60/12.66
WB'(N(z0, l, r)) → c42

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, MIN, MAX, BS', SIZE, WB'

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c30, c3, c6, c10, c13, c21, c29, c34, c36, c38, c40, c42

44.60/12.66

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

44.60/12.66

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.66
+(0, z0) → z0 44.60/12.66
+(z0, 0) → z0 44.60/12.66
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.66
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.66
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.66
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.66
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.66
-(z0, 0) → z0 44.60/12.66
-(0, z0) → 0 44.60/12.66
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.66
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.66
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.66
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.66
not(true) → false 44.60/12.66
not(false) → true 44.60/12.66
and(z0, true) → z0 44.60/12.66
and(z0, false) → false 44.60/12.66
if(true, z0, z1) → z0 44.60/12.66
if(false, z0, z1) → z1 44.60/12.66
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.66
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.66
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.66
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.66
ge(z0, 0) → true 44.60/12.66
ge(0, O(z0)) → ge(0, z0) 44.60/12.66
ge(0, I(z0)) → false 44.60/12.66
Log'(0) → 0 44.60/12.66
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.66
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.66
Log(z0) → -(Log'(z0), I(0)) 44.60/12.66
Val(L(z0)) → z0 44.60/12.66
Val(N(z0, l, r)) → z0 44.60/12.66
Min(L(z0)) → z0 44.60/12.66
Min(N(z0, l, r)) → Min(l) 44.60/12.66
Max(L(z0)) → z0 44.60/12.66
Max(N(z0, l, r)) → Max(r) 44.60/12.66
BS(L(z0)) → true 44.60/12.66
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.66
Size(L(z0)) → I(0) 44.60/12.66
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.66
WB(L(z0)) → true 44.60/12.66
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)) 44.60/12.66
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.66
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.66
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.66
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.66
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.66
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.66
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.66
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.66
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.66
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.66
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.66
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.66
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.66
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
MIN(N(z0, l, r)) → c34 44.60/12.66
MAX(N(z0, l, r)) → c36 44.60/12.66
BS'(N(z0, l, r)) → c38 44.60/12.66
SIZE(N(z0, l, r)) → c40 44.60/12.66
WB'(N(z0, l, r)) → c42 44.60/12.66
LOG(z0) → c(-'(Log'(z0), I(0))) 44.60/12.66
LOG(z0) → c(LOG'(z0))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.66
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.66
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.66
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.66
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.66
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.66
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.66
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.66
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.66
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.66
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.66
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.66
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.66
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.66
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
MIN(N(z0, l, r)) → c34 44.60/12.66
MAX(N(z0, l, r)) → c36 44.60/12.66
BS'(N(z0, l, r)) → c38 44.60/12.66
SIZE(N(z0, l, r)) → c40 44.60/12.66
WB'(N(z0, l, r)) → c42 44.60/12.66
LOG(z0) → c(-'(Log'(z0), I(0))) 44.60/12.66
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', MIN, MAX, BS', SIZE, WB', LOG

Compound Symbols:

c4, c5, c7, c11, c12, c20, c22, c23, c25, c28, c3, c6, c10, c13, c21, c29, c34, c36, c38, c40, c42, c

44.60/12.66

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

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

Removed 5 trailing nodes:

BS'(N(z0, l, r)) → c38 44.60/12.66
WB'(N(z0, l, r)) → c42 44.60/12.66
SIZE(N(z0, l, r)) → c40 44.60/12.66
MIN(N(z0, l, r)) → c34 44.60/12.66
MAX(N(z0, l, r)) → c36

44.60/12.66

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.66
+(0, z0) → z0 44.60/12.66
+(z0, 0) → z0 44.60/12.66
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.66
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.66
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.66
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.66
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.66
-(z0, 0) → z0 44.60/12.66
-(0, z0) → 0 44.60/12.66
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.66
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.66
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.66
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.66
not(true) → false 44.60/12.66
not(false) → true 44.60/12.66
and(z0, true) → z0 44.60/12.66
and(z0, false) → false 44.60/12.66
if(true, z0, z1) → z0 44.60/12.66
if(false, z0, z1) → z1 44.60/12.66
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.66
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.66
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.66
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.66
ge(z0, 0) → true 44.60/12.66
ge(0, O(z0)) → ge(0, z0) 44.60/12.66
ge(0, I(z0)) → false 44.60/12.66
Log'(0) → 0 44.60/12.66
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.66
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.66
Log(z0) → -(Log'(z0), I(0)) 44.60/12.66
Val(L(z0)) → z0 44.60/12.66
Val(N(z0, l, r)) → z0 44.60/12.66
Min(L(z0)) → z0 44.60/12.66
Min(N(z0, l, r)) → Min(l) 44.60/12.66
Max(L(z0)) → z0 44.60/12.66
Max(N(z0, l, r)) → Max(r) 44.60/12.66
BS(L(z0)) → true 44.60/12.66
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.66
Size(L(z0)) → I(0) 44.60/12.66
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.66
WB(L(z0)) → true 44.60/12.66
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)) 44.60/12.66
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.66
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.66
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.66
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.66
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.66
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.66
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.66
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.66
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.66
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.66
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.66
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.66
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.66
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.66
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.66
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.66
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.66
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.66
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.66
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.66
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.66
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.66
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.66
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.66
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.66
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.66
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.66
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.66
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

44.60/12.66

(9) 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)))

44.60/12.66

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.66
+(0, z0) → z0 44.60/12.66
+(z0, 0) → z0 44.60/12.66
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.67
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.67
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.67
-(z0, 0) → z0 44.60/12.67
-(0, z0) → 0 44.60/12.67
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.67
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.67
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.67
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.67
not(true) → false 44.60/12.67
not(false) → true 44.60/12.67
and(z0, true) → z0 44.60/12.67
and(z0, false) → false 44.60/12.67
if(true, z0, z1) → z0 44.60/12.67
if(false, z0, z1) → z1 44.60/12.67
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.67
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.67
ge(z0, 0) → true 44.60/12.67
ge(0, O(z0)) → ge(0, z0) 44.60/12.67
ge(0, I(z0)) → false 44.60/12.67
Log'(0) → 0 44.60/12.67
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.67
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.67
Log(z0) → -(Log'(z0), I(0)) 44.60/12.67
Val(L(z0)) → z0 44.60/12.67
Val(N(z0, l, r)) → z0 44.60/12.67
Min(L(z0)) → z0 44.60/12.67
Min(N(z0, l, r)) → Min(l) 44.60/12.67
Max(L(z0)) → z0 44.60/12.67
Max(N(z0, l, r)) → Max(r) 44.60/12.67
BS(L(z0)) → true 44.60/12.67
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.67
Size(L(z0)) → I(0) 44.60/12.67
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.67
WB(L(z0)) → true 44.60/12.67
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)) 44.60/12.67
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.67
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.67
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.67
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.67
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.67
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.67
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.67
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.67
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.67
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
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

44.60/12.67

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))

We considered the (Usable) Rules:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.67

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

44.60/12.67

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.67
+(0, z0) → z0 44.60/12.67
+(z0, 0) → z0 44.60/12.67
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.67
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.67
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.67
-(z0, 0) → z0 44.60/12.67
-(0, z0) → 0 44.60/12.67
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.67
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.67
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.67
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.67
not(true) → false 44.60/12.67
not(false) → true 44.60/12.67
and(z0, true) → z0 44.60/12.67
and(z0, false) → false 44.60/12.67
if(true, z0, z1) → z0 44.60/12.67
if(false, z0, z1) → z1 44.60/12.67
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.67
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.67
ge(z0, 0) → true 44.60/12.67
ge(0, O(z0)) → ge(0, z0) 44.60/12.67
ge(0, I(z0)) → false 44.60/12.67
Log'(0) → 0 44.60/12.67
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.67
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.67
Log(z0) → -(Log'(z0), I(0)) 44.60/12.67
Val(L(z0)) → z0 44.60/12.67
Val(N(z0, l, r)) → z0 44.60/12.67
Min(L(z0)) → z0 44.60/12.67
Min(N(z0, l, r)) → Min(l) 44.60/12.67
Max(L(z0)) → z0 44.60/12.67
Max(N(z0, l, r)) → Max(r) 44.60/12.67
BS(L(z0)) → true 44.60/12.67
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.67
Size(L(z0)) → I(0) 44.60/12.67
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.67
WB(L(z0)) → true 44.60/12.67
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)) 44.60/12.67
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.67
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.67
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.67
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.67
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.67
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.67
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.67
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.67
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))

K tuples:

LOG(z0) → c(-'(Log'(z0), I(0))) 44.60/12.67
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1))

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

44.60/12.67

(13) CdtPolyRedPairProof (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)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))

We considered the (Usable) Rules:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.67

POL(+(x₁, x₂)) = [2]x₂ 44.60/12.67
POL(+'(x₁, x₂)) = 0 44.60/12.67
POL(-(x₁, x₂)) = 0 44.60/12.67
POL(-'(x₁, x₂)) = [2]x₂ 44.60/12.67
POL(0) = 0 44.60/12.67
POL(1) = 0 44.60/12.67
POL(GE(x₁, x₂)) = [2]x₁ + [4]x₂ 44.60/12.67
POL(I(x₁)) = x₁ 44.60/12.67
POL(LOG(x₁)) = [3] + [3]x₁ 44.60/12.67
POL(LOG'(x₁)) = x₁ 44.60/12.67
POL(Log'(x₁)) = 0 44.60/12.67
POL(O(x₁)) = [4] + [4]x₁ 44.60/12.67
POL(c(x₁)) = x₁ 44.60/12.67
POL(c10(x₁)) = x₁ 44.60/12.67
POL(c11(x₁, x₂)) = x₁ + x₂ 44.60/12.67
POL(c12(x₁)) = x₁ 44.60/12.67
POL(c13(x₁)) = x₁ 44.60/12.67
POL(c20(x₁)) = x₁ 44.60/12.67
POL(c21(x₁)) = x₁ 44.60/12.67
POL(c22(x₁)) = x₁ 44.60/12.67
POL(c23(x₁)) = x₁ 44.60/12.67
POL(c25(x₁)) = x₁ 44.60/12.67
POL(c28(x₁, x₂)) = x₁ + x₂ 44.60/12.67
POL(c29(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 44.60/12.67
POL(c3(x₁)) = x₁ 44.60/12.67
POL(c4(x₁)) = x₁ 44.60/12.67
POL(c5(x₁)) = x₁ 44.60/12.67
POL(c6(x₁, x₂)) = x₁ + x₂ 44.60/12.67
POL(c7(x₁, x₂)) = x₁ + x₂ 44.60/12.67
POL(false) = 0 44.60/12.67
POL(ge(x₁, x₂)) = [4] + [2]x₁ + [4]x₂ 44.60/12.67
POL(if(x₁, x₂, x₃)) = [3] + [3]x₂ + [3]x₃ 44.60/12.67
POL(not(x₁)) = [4] + [2]x₁ 44.60/12.67
POL(true) = [2]

44.60/12.67

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.67
+(0, z0) → z0 44.60/12.67
+(z0, 0) → z0 44.60/12.67
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.67
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.67
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.67
-(z0, 0) → z0 44.60/12.67
-(0, z0) → 0 44.60/12.67
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.67
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.67
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.67
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.67
not(true) → false 44.60/12.67
not(false) → true 44.60/12.67
and(z0, true) → z0 44.60/12.67
and(z0, false) → false 44.60/12.67
if(true, z0, z1) → z0 44.60/12.67
if(false, z0, z1) → z1 44.60/12.67
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.67
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.67
ge(z0, 0) → true 44.60/12.67
ge(0, O(z0)) → ge(0, z0) 44.60/12.67
ge(0, I(z0)) → false 44.60/12.67
Log'(0) → 0 44.60/12.67
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.67
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.67
Log(z0) → -(Log'(z0), I(0)) 44.60/12.67
Val(L(z0)) → z0 44.60/12.67
Val(N(z0, l, r)) → z0 44.60/12.67
Min(L(z0)) → z0 44.60/12.67
Min(N(z0, l, r)) → Min(l) 44.60/12.67
Max(L(z0)) → z0 44.60/12.67
Max(N(z0, l, r)) → Max(r) 44.60/12.67
BS(L(z0)) → true 44.60/12.67
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.67
Size(L(z0)) → I(0) 44.60/12.67
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.67
WB(L(z0)) → true 44.60/12.67
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)) 44.60/12.67
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.67
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.67
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.67
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.67
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.67
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.67
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.67
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.67
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.67
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.67
-'(I(z0), I(z1)) → c13(-'(z0, z1))

K tuples:

LOG(z0) → c(-'(Log'(z0), I(0))) 44.60/12.67
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.67
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0))

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

44.60/12.67

(15) CdtPolyRedPairProof (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:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.67

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

44.60/12.67

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.67
+(0, z0) → z0 44.60/12.67
+(z0, 0) → z0 44.60/12.67
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.67
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.67
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.67
-(z0, 0) → z0 44.60/12.67
-(0, z0) → 0 44.60/12.67
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.67
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.67
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.67
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.67
not(true) → false 44.60/12.67
not(false) → true 44.60/12.67
and(z0, true) → z0 44.60/12.67
and(z0, false) → false 44.60/12.67
if(true, z0, z1) → z0 44.60/12.67
if(false, z0, z1) → z1 44.60/12.67
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.67
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.67
ge(z0, 0) → true 44.60/12.67
ge(0, O(z0)) → ge(0, z0) 44.60/12.67
ge(0, I(z0)) → false 44.60/12.67
Log'(0) → 0 44.60/12.67
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.67
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.67
Log(z0) → -(Log'(z0), I(0)) 44.60/12.67
Val(L(z0)) → z0 44.60/12.67
Val(N(z0, l, r)) → z0 44.60/12.67
Min(L(z0)) → z0 44.60/12.67
Min(N(z0, l, r)) → Min(l) 44.60/12.67
Max(L(z0)) → z0 44.60/12.67
Max(N(z0, l, r)) → Max(r) 44.60/12.67
BS(L(z0)) → true 44.60/12.67
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.67
Size(L(z0)) → I(0) 44.60/12.67
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.67
WB(L(z0)) → true 44.60/12.67
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)) 44.60/12.67
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.67
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.67
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.67
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.67
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.67
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.67
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.67
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.67
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.67
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.67
-'(I(z0), I(z1)) → c13(-'(z0, z1))

K tuples:

LOG(z0) → c(-'(Log'(z0), I(0))) 44.60/12.67
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.67
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.67
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.67
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.67
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.67
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.67
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.67
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.67
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0))

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

44.60/12.67

(17) CdtPolyRedPairProof (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:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.67

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

44.60/12.67

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.67
+(0, z0) → z0 44.60/12.67
+(z0, 0) → z0 44.60/12.67
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.67
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.67
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.67
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.67
-(z0, 0) → z0 44.60/12.67
-(0, z0) → 0 44.60/12.67
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.67
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.67
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.67
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.67
not(true) → false 44.60/12.67
not(false) → true 44.60/12.67
and(z0, true) → z0 44.60/12.67
and(z0, false) → false 44.60/12.67
if(true, z0, z1) → z0 44.60/12.67
if(false, z0, z1) → z1 44.60/12.67
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.67
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.67
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.67
ge(z0, 0) → true 44.60/12.67
ge(0, O(z0)) → ge(0, z0) 44.60/12.67
ge(0, I(z0)) → false 44.60/12.67
Log'(0) → 0 44.60/12.67
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.67
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.67
Log(z0) → -(Log'(z0), I(0)) 44.60/12.67
Val(L(z0)) → z0 44.60/12.67
Val(N(z0, l, r)) → z0 44.60/12.67
Min(L(z0)) → z0 44.60/12.67
Min(N(z0, l, r)) → Min(l) 44.60/12.67
Max(L(z0)) → z0 44.60/12.67
Max(N(z0, l, r)) → Max(r) 44.60/12.67
BS(L(z0)) → true 44.60/12.67
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.67
Size(L(z0)) → I(0) 44.60/12.67
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.67
WB(L(z0)) → true 44.60/12.67
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)) 44.60/12.68
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.68
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.68
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.68
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.68
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.68
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.68
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.68
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.68
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.68
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.68
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.68
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.68
-'(I(z0), I(z1)) → c13(-'(z0, z1))

K tuples:

LOG(z0) → c(-'(Log'(z0), I(0))) 44.60/12.68
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.68
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.68
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.68
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.68
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.68
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.68
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.68
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
GE(I(z0), I(z1)) → c23(GE(z0, z1))

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

44.60/12.68

(19) CdtPolyRedPairProof (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)) 44.60/12.68
+'(O(z0), O(z1)) → c3(+'(z0, z1))

We considered the (Usable) Rules:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.68

POL(+(x₁, x₂)) = [4]x₁ + [2]x₂ 44.60/12.68
POL(+'(x₁, x₂)) = x₂ 44.60/12.68
POL(-(x₁, x₂)) = 0 44.60/12.68
POL(-'(x₁, x₂)) = 0 44.60/12.68
POL(0) = 0 44.60/12.68
POL(1) = 0 44.60/12.68
POL(GE(x₁, x₂)) = [1] + x₁ + [2]x₂ 44.60/12.68
POL(I(x₁)) = x₁ 44.60/12.68
POL(LOG(x₁)) = [4] + [4]x₁ 44.60/12.68
POL(LOG'(x₁)) = [2]x₁ 44.60/12.68
POL(Log'(x₁)) = 0 44.60/12.68
POL(O(x₁)) = [1] + [4]x₁ 44.60/12.68
POL(c(x₁)) = x₁ 44.60/12.68
POL(c10(x₁)) = x₁ 44.60/12.68
POL(c11(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c12(x₁)) = x₁ 44.60/12.68
POL(c13(x₁)) = x₁ 44.60/12.68
POL(c20(x₁)) = x₁ 44.60/12.68
POL(c21(x₁)) = x₁ 44.60/12.68
POL(c22(x₁)) = x₁ 44.60/12.68
POL(c23(x₁)) = x₁ 44.60/12.68
POL(c25(x₁)) = x₁ 44.60/12.68
POL(c28(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c29(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 44.60/12.68
POL(c3(x₁)) = x₁ 44.60/12.68
POL(c4(x₁)) = x₁ 44.60/12.68
POL(c5(x₁)) = x₁ 44.60/12.68
POL(c6(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c7(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(false) = 0 44.60/12.68
POL(ge(x₁, x₂)) = 0 44.60/12.68
POL(if(x₁, x₂, x₃)) = [3] + [3]x₂ + [3]x₃ 44.60/12.68
POL(not(x₁)) = [3] + [3]x₁ 44.60/12.68
POL(true) = 0

44.60/12.68

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.68
+(0, z0) → z0 44.60/12.68
+(z0, 0) → z0 44.60/12.68
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.68
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.68
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.68
-(z0, 0) → z0 44.60/12.68
-(0, z0) → 0 44.60/12.68
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.68
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.68
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.68
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.68
not(true) → false 44.60/12.68
not(false) → true 44.60/12.68
and(z0, true) → z0 44.60/12.68
and(z0, false) → false 44.60/12.68
if(true, z0, z1) → z0 44.60/12.68
if(false, z0, z1) → z1 44.60/12.68
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.68
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.68
ge(z0, 0) → true 44.60/12.68
ge(0, O(z0)) → ge(0, z0) 44.60/12.68
ge(0, I(z0)) → false 44.60/12.68
Log'(0) → 0 44.60/12.68
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.68
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.68
Log(z0) → -(Log'(z0), I(0)) 44.60/12.68
Val(L(z0)) → z0 44.60/12.68
Val(N(z0, l, r)) → z0 44.60/12.68
Min(L(z0)) → z0 44.60/12.68
Min(N(z0, l, r)) → Min(l) 44.60/12.68
Max(L(z0)) → z0 44.60/12.68
Max(N(z0, l, r)) → Max(r) 44.60/12.68
BS(L(z0)) → true 44.60/12.68
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.68
Size(L(z0)) → I(0) 44.60/12.68
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.68
WB(L(z0)) → true 44.60/12.68
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)) 44.60/12.68
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.68
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.68
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.68
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.68
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.68
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.68
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.68
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.68
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.68
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.68
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.68
-'(I(z0), I(z1)) → c13(-'(z0, z1))

K tuples:

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

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

44.60/12.68

(21) CdtPolyRedPairProof (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:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.68

POL(+(x₁, x₂)) = 0 44.60/12.68
POL(+'(x₁, x₂)) = 0 44.60/12.68
POL(-(x₁, x₂)) = 0 44.60/12.68
POL(-'(x₁, x₂)) = x₂ 44.60/12.68
POL(0) = 0 44.60/12.68
POL(1) = 0 44.60/12.68
POL(GE(x₁, x₂)) = 0 44.60/12.68
POL(I(x₁)) = [1] + x₁ 44.60/12.68
POL(LOG(x₁)) = [3] 44.60/12.68
POL(LOG'(x₁)) = [4]x₁ 44.60/12.68
POL(Log'(x₁)) = 0 44.60/12.68
POL(O(x₁)) = [2] + [4]x₁ 44.60/12.68
POL(c(x₁)) = x₁ 44.60/12.68
POL(c10(x₁)) = x₁ 44.60/12.68
POL(c11(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c12(x₁)) = x₁ 44.60/12.68
POL(c13(x₁)) = x₁ 44.60/12.68
POL(c20(x₁)) = x₁ 44.60/12.68
POL(c21(x₁)) = x₁ 44.60/12.68
POL(c22(x₁)) = x₁ 44.60/12.68
POL(c23(x₁)) = x₁ 44.60/12.68
POL(c25(x₁)) = x₁ 44.60/12.68
POL(c28(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c29(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 44.60/12.68
POL(c3(x₁)) = x₁ 44.60/12.68
POL(c4(x₁)) = x₁ 44.60/12.68
POL(c5(x₁)) = x₁ 44.60/12.68
POL(c6(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c7(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(false) = 0 44.60/12.68
POL(ge(x₁, x₂)) = [4] + [2]x₁ + [4]x₂ 44.60/12.68
POL(if(x₁, x₂, x₃)) = [3] + [3]x₂ + [3]x₃ 44.60/12.68
POL(not(x₁)) = [4] + [2]x₁ 44.60/12.68
POL(true) = [2]

44.60/12.68

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.68
+(0, z0) → z0 44.60/12.68
+(z0, 0) → z0 44.60/12.68
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.68
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.68
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.68
-(z0, 0) → z0 44.60/12.68
-(0, z0) → 0 44.60/12.68
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.68
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.68
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.68
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.68
not(true) → false 44.60/12.68
not(false) → true 44.60/12.68
and(z0, true) → z0 44.60/12.68
and(z0, false) → false 44.60/12.68
if(true, z0, z1) → z0 44.60/12.68
if(false, z0, z1) → z1 44.60/12.68
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.68
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.68
ge(z0, 0) → true 44.60/12.68
ge(0, O(z0)) → ge(0, z0) 44.60/12.68
ge(0, I(z0)) → false 44.60/12.68
Log'(0) → 0 44.60/12.68
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.68
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.68
Log(z0) → -(Log'(z0), I(0)) 44.60/12.68
Val(L(z0)) → z0 44.60/12.68
Val(N(z0, l, r)) → z0 44.60/12.68
Min(L(z0)) → z0 44.60/12.68
Min(N(z0, l, r)) → Min(l) 44.60/12.68
Max(L(z0)) → z0 44.60/12.68
Max(N(z0, l, r)) → Max(r) 44.60/12.68
BS(L(z0)) → true 44.60/12.68
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.68
Size(L(z0)) → I(0) 44.60/12.68
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.68
WB(L(z0)) → true 44.60/12.68
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)) 44.60/12.68
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.68
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.68
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.68
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.68
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.68
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.68
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.68
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.68
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.68
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.68
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(O(z0), I(z1)) → c4(+'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

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

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

44.60/12.68

(23) CdtPolyRedPairProof (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:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.68

POL(+(x₁, x₂)) = [2] + [4]x₁ + [4]x₂ 44.60/12.68
POL(+'(x₁, x₂)) = [4]x₂ 44.60/12.68
POL(-(x₁, x₂)) = 0 44.60/12.68
POL(-'(x₁, x₂)) = 0 44.60/12.68
POL(0) = 0 44.60/12.68
POL(1) = 0 44.60/12.68
POL(GE(x₁, x₂)) = 0 44.60/12.68
POL(I(x₁)) = [2] + x₁ 44.60/12.68
POL(LOG(x₁)) = [4] + [3]x₁ 44.60/12.68
POL(LOG'(x₁)) = [4]x₁ 44.60/12.68
POL(Log'(x₁)) = 0 44.60/12.68
POL(O(x₁)) = [2] + [2]x₁ 44.60/12.68
POL(c(x₁)) = x₁ 44.60/12.68
POL(c10(x₁)) = x₁ 44.60/12.68
POL(c11(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c12(x₁)) = x₁ 44.60/12.68
POL(c13(x₁)) = x₁ 44.60/12.68
POL(c20(x₁)) = x₁ 44.60/12.68
POL(c21(x₁)) = x₁ 44.60/12.68
POL(c22(x₁)) = x₁ 44.60/12.68
POL(c23(x₁)) = x₁ 44.60/12.68
POL(c25(x₁)) = x₁ 44.60/12.68
POL(c28(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c29(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 44.60/12.68
POL(c3(x₁)) = x₁ 44.60/12.68
POL(c4(x₁)) = x₁ 44.60/12.68
POL(c5(x₁)) = x₁ 44.60/12.68
POL(c6(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c7(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(false) = 0 44.60/12.68
POL(ge(x₁, x₂)) = 0 44.60/12.68
POL(if(x₁, x₂, x₃)) = [3] + [3]x₂ + [3]x₃ 44.60/12.68
POL(not(x₁)) = [3] + [3]x₁ 44.60/12.68
POL(true) = 0

44.60/12.68

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.68
+(0, z0) → z0 44.60/12.68
+(z0, 0) → z0 44.60/12.68
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.68
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.68
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.68
-(z0, 0) → z0 44.60/12.68
-(0, z0) → 0 44.60/12.68
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.68
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.68
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.68
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.68
not(true) → false 44.60/12.68
not(false) → true 44.60/12.68
and(z0, true) → z0 44.60/12.68
and(z0, false) → false 44.60/12.68
if(true, z0, z1) → z0 44.60/12.68
if(false, z0, z1) → z1 44.60/12.68
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.68
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.68
ge(z0, 0) → true 44.60/12.68
ge(0, O(z0)) → ge(0, z0) 44.60/12.68
ge(0, I(z0)) → false 44.60/12.68
Log'(0) → 0 44.60/12.68
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.68
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.68
Log(z0) → -(Log'(z0), I(0)) 44.60/12.68
Val(L(z0)) → z0 44.60/12.68
Val(N(z0, l, r)) → z0 44.60/12.68
Min(L(z0)) → z0 44.60/12.68
Min(N(z0, l, r)) → Min(l) 44.60/12.68
Max(L(z0)) → z0 44.60/12.68
Max(N(z0, l, r)) → Max(r) 44.60/12.68
BS(L(z0)) → true 44.60/12.68
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.68
Size(L(z0)) → I(0) 44.60/12.68
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.68
WB(L(z0)) → true 44.60/12.68
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)) 44.60/12.68
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.68
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.68
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.68
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.68
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.68
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.68
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.68
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.68
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.68
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.68
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

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

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

44.60/12.68

(25) CdtPolyRedPairProof (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:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.68

POL(+(x₁, x₂)) = x₁ + [2]x₂ 44.60/12.68
POL(+'(x₁, x₂)) = 0 44.60/12.68
POL(-(x₁, x₂)) = x₁ 44.60/12.68
POL(-'(x₁, x₂)) = x₁·x₂ 44.60/12.68
POL(0) = 0 44.60/12.68
POL(1) = 0 44.60/12.68
POL(GE(x₁, x₂)) = 0 44.60/12.68
POL(I(x₁)) = [2] + x₁ 44.60/12.68
POL(LOG(x₁)) = x₁ + [2]x₁² 44.60/12.68
POL(LOG'(x₁)) = 0 44.60/12.68
POL(Log'(x₁)) = x₁² 44.60/12.68
POL(O(x₁)) = [2] + x₁ 44.60/12.68
POL(c(x₁)) = x₁ 44.60/12.68
POL(c10(x₁)) = x₁ 44.60/12.68
POL(c11(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c12(x₁)) = x₁ 44.60/12.68
POL(c13(x₁)) = x₁ 44.60/12.68
POL(c20(x₁)) = x₁ 44.60/12.68
POL(c21(x₁)) = x₁ 44.60/12.68
POL(c22(x₁)) = x₁ 44.60/12.68
POL(c23(x₁)) = x₁ 44.60/12.68
POL(c25(x₁)) = x₁ 44.60/12.68
POL(c28(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c29(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 44.60/12.68
POL(c3(x₁)) = x₁ 44.60/12.68
POL(c4(x₁)) = x₁ 44.60/12.68
POL(c5(x₁)) = x₁ 44.60/12.68
POL(c6(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c7(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(false) = 0 44.60/12.68
POL(ge(x₁, x₂)) = 0 44.60/12.68
POL(if(x₁, x₂, x₃)) = x₂ + x₃ 44.60/12.68
POL(not(x₁)) = [3] + [3]x₁ + [3]x₁² 44.60/12.68
POL(true) = 0

44.60/12.68

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.68
+(0, z0) → z0 44.60/12.68
+(z0, 0) → z0 44.60/12.68
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.68
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.68
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.68
-(z0, 0) → z0 44.60/12.68
-(0, z0) → 0 44.60/12.68
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.68
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.68
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.68
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.68
not(true) → false 44.60/12.68
not(false) → true 44.60/12.68
and(z0, true) → z0 44.60/12.68
and(z0, false) → false 44.60/12.68
if(true, z0, z1) → z0 44.60/12.68
if(false, z0, z1) → z1 44.60/12.68
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.68
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.68
ge(z0, 0) → true 44.60/12.68
ge(0, O(z0)) → ge(0, z0) 44.60/12.68
ge(0, I(z0)) → false 44.60/12.68
Log'(0) → 0 44.60/12.68
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.68
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.68
Log(z0) → -(Log'(z0), I(0)) 44.60/12.68
Val(L(z0)) → z0 44.60/12.68
Val(N(z0, l, r)) → z0 44.60/12.68
Min(L(z0)) → z0 44.60/12.68
Min(N(z0, l, r)) → Min(l) 44.60/12.68
Max(L(z0)) → z0 44.60/12.68
Max(N(z0, l, r)) → Max(r) 44.60/12.68
BS(L(z0)) → true 44.60/12.68
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.68
Size(L(z0)) → I(0) 44.60/12.68
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.68
WB(L(z0)) → true 44.60/12.68
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)) 44.60/12.68
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.68
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.68
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.68
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.68
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.68
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.68
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.68
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.68
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.68
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.68
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:

+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

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

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

44.60/12.68

(27) CdtPolyRedPairProof (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:

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

And the Tuples:

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

The order we found is given by the following interpretation:
Polynomial interpretation : 44.60/12.68

POL(+(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(+'(x₁, x₂)) = x₂² + x₁·x₂ 44.60/12.68
POL(-(x₁, x₂)) = x₁ 44.60/12.68
POL(-'(x₁, x₂)) = x₁·x₂ 44.60/12.68
POL(0) = 0 44.60/12.68
POL(1) = 0 44.60/12.68
POL(GE(x₁, x₂)) = 0 44.60/12.68
POL(I(x₁)) = [2] + x₁ 44.60/12.68
POL(LOG(x₁)) = [3]x₁ 44.60/12.68
POL(LOG'(x₁)) = [2]x₁² 44.60/12.68
POL(Log'(x₁)) = x₁ 44.60/12.68
POL(O(x₁)) = [2] + x₁ 44.60/12.68
POL(c(x₁)) = x₁ 44.60/12.68
POL(c10(x₁)) = x₁ 44.60/12.68
POL(c11(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c12(x₁)) = x₁ 44.60/12.68
POL(c13(x₁)) = x₁ 44.60/12.68
POL(c20(x₁)) = x₁ 44.60/12.68
POL(c21(x₁)) = x₁ 44.60/12.68
POL(c22(x₁)) = x₁ 44.60/12.68
POL(c23(x₁)) = x₁ 44.60/12.68
POL(c25(x₁)) = x₁ 44.60/12.68
POL(c28(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c29(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 44.60/12.68
POL(c3(x₁)) = x₁ 44.60/12.68
POL(c4(x₁)) = x₁ 44.60/12.68
POL(c5(x₁)) = x₁ 44.60/12.68
POL(c6(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(c7(x₁, x₂)) = x₁ + x₂ 44.60/12.68
POL(false) = 0 44.60/12.68
POL(ge(x₁, x₂)) = [1] 44.60/12.68
POL(if(x₁, x₂, x₃)) = x₃ + x₁·x₂ 44.60/12.68
POL(not(x₁)) = [1] 44.60/12.68
POL(true) = [1]

44.60/12.68

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

O(0) → 0 44.60/12.68
+(0, z0) → z0 44.60/12.68
+(z0, 0) → z0 44.60/12.68
+(O(z0), O(z1)) → O(+(z0, z1)) 44.60/12.68
+(O(z0), I(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), O(z1)) → I(+(z0, z1)) 44.60/12.68
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0))) 44.60/12.68
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 44.60/12.68
-(z0, 0) → z0 44.60/12.68
-(0, z0) → 0 44.60/12.68
-(O(z0), O(z1)) → O(-(z0, z1)) 44.60/12.68
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1))) 44.60/12.68
-(I(z0), O(z1)) → I(-(z0, z1)) 44.60/12.68
-(I(z0), I(z1)) → O(-(z0, z1)) 44.60/12.68
not(true) → false 44.60/12.68
not(false) → true 44.60/12.68
and(z0, true) → z0 44.60/12.68
and(z0, false) → false 44.60/12.68
if(true, z0, z1) → z0 44.60/12.68
if(false, z0, z1) → z1 44.60/12.68
ge(O(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(O(z0), I(z1)) → not(ge(z1, z0)) 44.60/12.68
ge(I(z0), O(z1)) → ge(z0, z1) 44.60/12.68
ge(I(z0), I(z1)) → ge(z0, z1) 44.60/12.68
ge(z0, 0) → true 44.60/12.68
ge(0, O(z0)) → ge(0, z0) 44.60/12.68
ge(0, I(z0)) → false 44.60/12.68
Log'(0) → 0 44.60/12.68
Log'(I(z0)) → +(Log'(z0), I(0)) 44.60/12.68
Log'(O(z0)) → if(ge(z0, I(0)), +(Log'(z0), I(0)), 0) 44.60/12.68
Log(z0) → -(Log'(z0), I(0)) 44.60/12.68
Val(L(z0)) → z0 44.60/12.68
Val(N(z0, l, r)) → z0 44.60/12.68
Min(L(z0)) → z0 44.60/12.68
Min(N(z0, l, r)) → Min(l) 44.60/12.68
Max(L(z0)) → z0 44.60/12.68
Max(N(z0, l, r)) → Max(r) 44.60/12.68
BS(L(z0)) → true 44.60/12.68
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r))) 44.60/12.68
Size(L(z0)) → I(0) 44.60/12.68
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1)) 44.60/12.68
WB(L(z0)) → true 44.60/12.68
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)) 44.60/12.68
+'(I(z0), O(z1)) → c5(+'(z0, z1)) 44.60/12.68
+'(z0, +(z1, z2)) → c7(+'(+(z0, z1), z2), +'(z0, z1)) 44.60/12.68
-'(O(z0), I(z1)) → c11(-'(-(z0, z1), I(1)), -'(z0, z1)) 44.60/12.68
-'(I(z0), O(z1)) → c12(-'(z0, z1)) 44.60/12.68
GE(O(z0), O(z1)) → c20(GE(z0, z1)) 44.60/12.68
GE(I(z0), O(z1)) → c22(GE(z0, z1)) 44.60/12.68
GE(I(z0), I(z1)) → c23(GE(z0, z1)) 44.60/12.68
GE(0, O(z0)) → c25(GE(0, z0)) 44.60/12.68
LOG'(I(z0)) → c28(+'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
+'(O(z0), O(z1)) → c3(+'(z0, z1)) 44.60/12.68
+'(I(z0), I(z1)) → c6(+'(+(z0, z1), I(0)), +'(z0, z1)) 44.60/12.68
-'(O(z0), O(z1)) → c10(-'(z0, z1)) 44.60/12.68
-'(I(z0), I(z1)) → c13(-'(z0, z1)) 44.60/12.68
GE(O(z0), I(z1)) → c21(GE(z1, z0)) 44.60/12.68
LOG'(O(z0)) → c29(GE(z0, I(0)), +'(Log'(z0), I(0)), LOG'(z0)) 44.60/12.68
LOG(z0) → c(-'(Log'(z0), I(0)))

S tuples:none
K tuples:

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

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

44.60/12.68

(29) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

44.60/12.68

(30) BOUNDS(O(1), O(1))

44.60/12.68