Runtime Complexity (innermost) proof of /tmp/tmpLC

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

0 CpxTRS

↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CpxTRS

↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CdtProblem

↳9 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳10 CdtProblem

↳11 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳12 CdtProblem

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CdtProblem

↳15 CdtUsableRulesProof (⇔, 0 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 273 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 93 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 62 ms)

↳22 CdtProblem

↳23 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 67 ms)

↳24 CdtProblem

↳25 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 72 ms)

↳26 CdtProblem

↳27 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 743 ms)

↳28 CdtProblem

↳29 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 595 ms)

↳30 CdtProblem

↳31 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳32 BOUNDS(1, 1)

(0) Obligation:

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

The TRS R consists of the following rules:

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

Rewrite Strategy: INNERMOST

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

The following defined symbols can occur below the 0th argument of ge: Size, O, +, ge, -, not, Min, Max
The following defined symbols can occur below the 1th argument of ge: Size, O, +, ge, -, not, Max, Min
The following defined symbols can occur below the 0th argument of and: Size, O, +, if, ge, -, not, and, WB, Max, Min, BS
The following defined symbols can occur below the 1th argument of and: Size, O, +, if, ge, -, and, not, WB, Max, Min, BS
The following defined symbols can occur below the 0th argument of if: Size, O, +, ge, -, not
The following defined symbols can occur below the 1th argument of if: Size, O, +, ge, -, not
The following defined symbols can occur below the 2th argument of if: Size, O, +, ge, -, not
The following defined symbols can occur below the 0th argument of -: Size, O, +, ge, -, not, Log'
The following defined symbols can occur below the 1th argument of -: Size, O, +, ge, -, not
The following defined symbols can occur below the 0th argument of +: Size, O, +, ge, -, not, Log'
The following defined symbols can occur below the 1th argument of +: Size, O, +, ge, -, not
The following defined symbols can occur below the 0th argument of O: O, +, ge, -, not, Size, Log'
The following defined symbols can occur below the 0th argument of not: ge, not, Size, O, +, -, Min, Max

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
Log'(O(x)) → if(ge(x, I(0)), +(Log'(x), I(0)), 0)

(2) Obligation:

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

The TRS R consists of the following rules:

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

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
BS(L(z0)) → true
-(0, z0) → 0
-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
O(0) → 0
not(true) → false
not(false) → true
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
Size(L(z0)) → I(0)
Val(N(z0, l, r)) → z0
Val(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Min(L(z0)) → z0
and(z0, true) → z0
and(z0, false) → false
WB(L(z0)) → true
WB(N(z0, l, r)) → and(if(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), and(WB(l), WB(r)))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Log(z0) → -(Log'(z0), I(0))
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

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

S tuples:

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

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

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

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

Removed 26 trailing nodes:

+'(0, z0) → c17
-'(0, z0) → c9
GE(z0, 0) → c2
MIN(L(z0)) → c32
LOG'(0) → c40
WB'(N(z0, l, r)) → c36(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))
AND(z0, true) → c33
BS'(N(z0, l, r)) → c7(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))
-'(z0, 0) → c11
IF(true, z0, z1) → c37
IF(false, z0, z1) → c38
VAL(N(z0, l, r)) → c29
SIZE(N(z0, l, r)) → c27(+'(+(Size(l), Size(r)), I(1)), +'(Size(l), Size(r)), SIZE(l), SIZE(r))
WB'(L(z0)) → c35
MIN(N(z0, l, r)) → c31(MIN(l))
AND(z0, false) → c34
NOT(false) → c24
GE(0, I(z0)) → c1
MAX(L(z0)) → c25
VAL(L(z0)) → c30
MAX(N(z0, l, r)) → c26(MAX(r))
NOT(true) → c23
O'(0) → c22
BS'(L(z0)) → c8
+'(z0, 0) → c18
SIZE(L(z0)) → c28

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
BS(L(z0)) → true
-(0, z0) → 0
-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
O(0) → 0
not(true) → false
not(false) → true
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
Size(L(z0)) → I(0)
Val(N(z0, l, r)) → z0
Val(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Min(L(z0)) → z0
and(z0, true) → z0
and(z0, false) → false
WB(L(z0)) → true
WB(N(z0, l, r)) → and(if(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), and(WB(l), WB(r)))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Log(z0) → -(Log'(z0), I(0))
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(O(z0), I(z1)) → c4(NOT(ge(z1, z0)), GE(z1, z0))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(O'(-(z0, z1)), -'(z0, z1))
-'(O(z0), O(z1)) → c13(O'(-(z0, z1)), -'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(O(z0), O(z1)) → c19(O'(+(z0, z1)), +'(z0, z1))
+'(I(z0), I(z1)) → c20(O'(+(+(z0, z1), I(0))), +'(+(z0, z1), I(0)), +'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG(z0) → c39(-'(Log'(z0), I(0)), LOG'(z0))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))

S tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(O(z0), I(z1)) → c4(NOT(ge(z1, z0)), GE(z1, z0))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(O'(-(z0, z1)), -'(z0, z1))
-'(O(z0), O(z1)) → c13(O'(-(z0, z1)), -'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(O(z0), O(z1)) → c19(O'(+(z0, z1)), +'(z0, z1))
+'(I(z0), I(z1)) → c20(O'(+(+(z0, z1), I(0))), +'(+(z0, z1), I(0)), +'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG(z0) → c39(-'(Log'(z0), I(0)), LOG'(z0))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c4, c5, c6, c10, c12, c13, c14, c15, c16, c19, c20, c21, c39, c41

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

Removed 5 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
BS(L(z0)) → true
-(0, z0) → 0
-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
O(0) → 0
not(true) → false
not(false) → true
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
Size(L(z0)) → I(0)
Val(N(z0, l, r)) → z0
Val(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Min(L(z0)) → z0
and(z0, true) → z0
and(z0, false) → false
WB(L(z0)) → true
WB(N(z0, l, r)) → and(if(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), and(WB(l), WB(r)))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Log(z0) → -(Log'(z0), I(0))
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG(z0) → c39(-'(Log'(z0), I(0)), LOG'(z0))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

S tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG(z0) → c39(-'(Log'(z0), I(0)), LOG'(z0))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c39, c41, c4, c12, c13, c19, c20

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

Split RHS of tuples not part of any SCC

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
BS(L(z0)) → true
-(0, z0) → 0
-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
O(0) → 0
not(true) → false
not(false) → true
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
Size(L(z0)) → I(0)
Val(N(z0, l, r)) → z0
Val(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Min(L(z0)) → z0
and(z0, true) → z0
and(z0, false) → false
WB(L(z0)) → true
WB(N(z0, l, r)) → and(if(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), and(WB(l), WB(r)))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Log(z0) → -(Log'(z0), I(0))
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG(z0) → c1(LOG'(z0))

S tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG(z0) → c1(LOG'(z0))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

LOG(z0) → c1(LOG'(z0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
BS(L(z0)) → true
-(0, z0) → 0
-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
O(0) → 0
not(true) → false
not(false) → true
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
Size(L(z0)) → I(0)
Val(N(z0, l, r)) → z0
Val(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Min(L(z0)) → z0
and(z0, true) → z0
and(z0, false) → false
WB(L(z0)) → true
WB(N(z0, l, r)) → and(if(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), and(WB(l), WB(r)))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Log(z0) → -(Log'(z0), I(0))
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

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

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

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
BS(L(z0)) → true
-(0, z0) → 0
-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(z0, 0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
O(0) → 0
not(true) → false
not(false) → true
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
Size(L(z0)) → I(0)
Val(N(z0, l, r)) → z0
Val(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Min(L(z0)) → z0
and(z0, true) → z0
and(z0, false) → false
WB(L(z0)) → true
WB(N(z0, l, r)) → and(if(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), and(WB(l), WB(r)))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Log(z0) → -(Log'(z0), I(0))
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

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

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

(15) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

ge(0, O(z0)) → ge(0, z0)
ge(0, I(z0)) → false
ge(z0, 0) → true
ge(O(z0), O(z1)) → ge(z0, z1)
ge(O(z0), I(z1)) → not(ge(z1, z0))
ge(I(z0), O(z1)) → ge(z0, z1)
ge(I(z0), I(z1)) → ge(z0, z1)
BS(N(z0, l, r)) → and(and(ge(z0, Max(l)), ge(Min(r), z0)), and(BS(l), BS(r)))
BS(L(z0)) → true
not(true) → false
not(false) → true
Max(L(z0)) → z0
Max(N(z0, l, r)) → Max(r)
Size(N(z0, l, r)) → +(+(Size(l), Size(r)), I(1))
Size(L(z0)) → I(0)
Val(N(z0, l, r)) → z0
Val(L(z0)) → z0
Min(N(z0, l, r)) → Min(l)
Min(L(z0)) → z0
and(z0, true) → z0
and(z0, false) → false
WB(L(z0)) → true
WB(N(z0, l, r)) → and(if(ge(Size(l), Size(r)), ge(I(0), -(Size(l), Size(r))), ge(I(0), -(Size(r), Size(l)))), and(WB(l), WB(r)))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
Log(z0) → -(Log'(z0), I(0))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(0, z0) → 0
O(0) → 0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

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

Defined Rule Symbols:

-, O, +, Log'

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

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

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

LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))

We considered the (Usable) Rules:none
And the Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

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

POL(+(x₁, x₂)) = x₂
POL(+'(x₁, x₂)) = 0
POL(-(x₁, x₂)) = 0
POL(-'(x₁, x₂)) = 0
POL(0) = 0
POL(1) = 0
POL(GE(x₁, x₂)) = 0
POL(I(x₁)) = [1] + x₁
POL(LOG(x₁)) = [1] + x₁
POL(LOG'(x₁)) = x₁
POL(Log'(x₁)) = [1] + x₁
POL(O(x₁)) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c21(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c41(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(0, z0) → 0
O(0) → 0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))

Defined Rule Symbols:

-, O, +, Log'

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

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

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

-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

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

POL(+(x₁, x₂)) = x₂
POL(+'(x₁, x₂)) = 0
POL(-(x₁, x₂)) = 0
POL(-'(x₁, x₂)) = x₂
POL(0) = 0
POL(1) = 0
POL(GE(x₁, x₂)) = 0
POL(I(x₁)) = [1] + x₁
POL(LOG(x₁)) = [1] + x₁
POL(LOG'(x₁)) = 0
POL(Log'(x₁)) = [1] + x₁
POL(O(x₁)) = [1] + x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c21(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c41(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(0, z0) → 0
O(0) → 0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))

Defined Rule Symbols:

-, O, +, Log'

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

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

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

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
GE(O(z0), I(z1)) → c4(GE(z1, z0))

We considered the (Usable) Rules:none
And the Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

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

POL(+(x₁, x₂)) = 0
POL(+'(x₁, x₂)) = 0
POL(-(x₁, x₂)) = 0
POL(-'(x₁, x₂)) = x₂
POL(0) = 0
POL(1) = 0
POL(GE(x₁, x₂)) = x₁ + x₂
POL(I(x₁)) = [1] + x₁
POL(LOG(x₁)) = [1]
POL(LOG'(x₁)) = x₁
POL(Log'(x₁)) = 0
POL(O(x₁)) = [1] + x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c21(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c41(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(0, z0) → 0
O(0) → 0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
GE(O(z0), I(z1)) → c4(GE(z1, z0))

Defined Rule Symbols:

-, O, +, Log'

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

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

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

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

We considered the (Usable) Rules:none
And the Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

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

POL(+(x₁, x₂)) = [1] + x₁ + x₂
POL(+'(x₁, x₂)) = x₂
POL(-(x₁, x₂)) = [1]
POL(-'(x₁, x₂)) = 0
POL(0) = 0
POL(1) = 0
POL(GE(x₁, x₂)) = x₁ + x₂
POL(I(x₁)) = x₁
POL(LOG(x₁)) = x₁
POL(LOG'(x₁)) = 0
POL(Log'(x₁)) = 0
POL(O(x₁)) = x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c21(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c41(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(0, z0) → 0
O(0) → 0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))

Defined Rule Symbols:

-, O, +, Log'

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

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

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

+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

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

POL(+(x₁, x₂)) = [1] + x₁ + x₂
POL(+'(x₁, x₂)) = x₂
POL(-(x₁, x₂)) = [1]
POL(-'(x₁, x₂)) = 0
POL(0) = 0
POL(1) = 0
POL(GE(x₁, x₂)) = 0
POL(I(x₁)) = [1] + x₁
POL(LOG(x₁)) = [1] + x₁
POL(LOG'(x₁)) = x₁
POL(Log'(x₁)) = 0
POL(O(x₁)) = [1] + x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c21(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c41(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(0, z0) → 0
O(0) → 0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

K tuples:

LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))

Defined Rule Symbols:

-, O, +, Log'

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

(27) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

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

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

We considered the (Usable) Rules:

+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(O(z0), O(z1)) → O(+(z0, z1))
O(0) → 0
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
Log'(0) → 0
+(0, z0) → z0
Log'(I(z0)) → +(Log'(z0), I(0))
+(z0, 0) → z0

And the Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

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

POL(+(x₁, x₂)) = x₁ + x₂
POL(+'(x₁, x₂)) = x₂² + [2]x₁·x₂
POL(-(x₁, x₂)) = 0
POL(-'(x₁, x₂)) = 0
POL(0) = 0
POL(1) = 0
POL(GE(x₁, x₂)) = 0
POL(I(x₁)) = [2] + x₁
POL(LOG(x₁)) = [1] + x₁ + [2]x₁²
POL(LOG'(x₁)) = [2]x₁ + [2]x₁²
POL(Log'(x₁)) = [2] + x₁
POL(O(x₁)) = x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c21(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c41(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(0, z0) → 0
O(0) → 0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:

-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))

K tuples:

LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))

Defined Rule Symbols:

-, O, +, Log'

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

(29) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

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

-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))

We considered the (Usable) Rules:

+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
-(0, z0) → 0
-(I(z0), I(z1)) → O(-(z0, z1))
+(O(z0), O(z1)) → O(+(z0, z1))
O(0) → 0
-(O(z0), O(z1)) → O(-(z0, z1))
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))
-(I(z0), O(z1)) → I(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(z0, 0) → z0
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(0, z0) → z0
+(z0, 0) → z0

And the Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

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

POL(+(x₁, x₂)) = x₁ + x₂
POL(+'(x₁, x₂)) = x₂²
POL(-(x₁, x₂)) = x₁
POL(-'(x₁, x₂)) = [2]x₁·x₂
POL(0) = 0
POL(1) = 0
POL(GE(x₁, x₂)) = 0
POL(I(x₁)) = [1] + x₁
POL(LOG(x₁)) = [2] + x₁ + [2]x₁²
POL(LOG'(x₁)) = x₁
POL(Log'(x₁)) = x₁²
POL(O(x₁)) = [1] + x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c21(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c41(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

-(I(z0), O(z1)) → I(-(z0, z1))
-(z0, 0) → z0
-(I(z0), I(z1)) → O(-(z0, z1))
-(O(z0), O(z1)) → O(-(z0, z1))
-(O(z0), I(z1)) → I(-(-(z0, z1), I(1)))
-(0, z0) → 0
O(0) → 0
+(O(z0), I(z1)) → I(+(z0, z1))
+(I(z0), O(z1)) → I(+(z0, z1))
+(0, z0) → z0
+(O(z0), O(z1)) → O(+(z0, z1))
+(I(z0), I(z1)) → O(+(+(z0, z1), I(0)))
+(z0, +(z1, z2)) → +(+(z0, z1), z2)
+(z0, 0) → z0
Log'(0) → 0
Log'(I(z0)) → +(Log'(z0), I(0))

Tuples:

GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
LOG(z0) → c1(-'(Log'(z0), I(0)))

S tuples:none
K tuples:

LOG(z0) → c1(-'(Log'(z0), I(0)))
LOG'(I(z0)) → c41(+'(Log'(z0), I(0)), LOG'(z0))
-'(I(z0), O(z1)) → c10(-'(z0, z1))
-'(I(z0), I(z1)) → c12(-'(z0, z1))
-'(O(z0), O(z1)) → c13(-'(z0, z1))
GE(0, O(z0)) → c(GE(0, z0))
GE(O(z0), O(z1)) → c3(GE(z0, z1))
GE(I(z0), O(z1)) → c5(GE(z0, z1))
GE(I(z0), I(z1)) → c6(GE(z0, z1))
GE(O(z0), I(z1)) → c4(GE(z1, z0))
+'(z0, +(z1, z2)) → c21(+'(+(z0, z1), z2), +'(z0, z1))
+'(O(z0), I(z1)) → c15(+'(z0, z1))
+'(I(z0), O(z1)) → c16(+'(z0, z1))
+'(O(z0), O(z1)) → c19(+'(z0, z1))
+'(I(z0), I(z1)) → c20(+'(+(z0, z1), I(0)), +'(z0, z1))
-'(O(z0), I(z1)) → c14(-'(-(z0, z1), I(1)), -'(z0, z1))

Defined Rule Symbols:

-, O, +, Log'

Defined Pair Symbols:

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

Compound Symbols:

c, c3, c5, c6, c10, c14, c15, c16, c21, c41, c4, c12, c13, c19, c20, c1

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

The set S is empty

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(12) Obligation:

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtUsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

(27) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(28) Obligation:

(29) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(30) Obligation:

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

(32) BOUNDS(1, 1)