YES(O(1), O(n^2)) 9.09/2.76 YES(O(1), O(n^2)) 9.09/2.79 9.09/2.79 9.09/2.79 9.09/2.79 9.09/2.79 9.09/2.79 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 9.09/2.79 9.09/2.79 9.09/2.79
9.09/2.79
9.09/2.79
9.09/2.79
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxRelTRS
9.09/2.79 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
9.09/2.79 
↳2 CdtProblem
9.09/2.79 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
9.09/2.79 
↳4 CdtProblem
9.09/2.79 
↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
9.09/2.79 
↳6 CdtProblem
9.09/2.79 
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)
9.09/2.79 
↳8 CdtProblem
9.09/2.79 
↳9 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
9.09/2.79 
↳10 CdtProblem
9.09/2.79 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
9.09/2.79 
↳12 CdtProblem
9.09/2.79 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
9.09/2.79 
↳14 CdtProblem
9.09/2.79 
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
9.09/2.79 
↳16 CdtProblem
9.09/2.79 
↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID))
9.09/2.79 
↳18 BOUNDS(O(1), O(1))
9.09/2.79
9.09/2.79 9.09/2.79
9.09/2.79
9.09/2.79

(0) Obligation:

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

bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs)) 9.09/2.79
len(Cons(x, xs)) → +(S(0), len(xs)) 9.09/2.79
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 9.09/2.79
len(Nil) → 0 9.09/2.79
bubble(x, Nil) → Cons(x, Nil) 9.09/2.79
bsort(0, xs) → xs 9.09/2.79
bubblesort(xs) → bsort(len(xs), xs)

The (relative) TRS S consists of the following rules:

+(x, S(0)) → S(x) 9.09/2.79
+(S(0), y) → S(y) 9.09/2.79
<(S(x), S(y)) → <(x, y) 9.09/2.79
<(0, S(y)) → True 9.09/2.79
<(x, 0) → False 9.09/2.79
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs)) 9.09/2.79
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Rewrite Strategy: INNERMOST
9.09/2.79
9.09/2.79

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
9.09/2.79
9.09/2.79

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0) 9.09/2.79
+(S(0), z0) → S(z0) 9.09/2.79
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.80
<(0, S(z0)) → True 9.49/2.80
<(z0, 0) → False 9.49/2.80
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.80
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2)) 9.49/2.80
bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2)) 9.49/2.80
bsort(0, z0) → z0 9.49/2.80
len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.80
len(Nil) → 0 9.49/2.80
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.80
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.80
bubblesort(z0) → bsort(len(z0), z0)
Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.80
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.80
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.80
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.80
LEN(Cons(z0, z1)) → c9(+'(S(0), len(z1)), LEN(z1)) 9.49/2.80
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.80
BUBBLESORT(z0) → c13(BSORT(len(z0), z0), LEN(z0))
S tuples:

BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.80
LEN(Cons(z0, z1)) → c9(+'(S(0), len(z1)), LEN(z1)) 9.49/2.80
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.80
BUBBLESORT(z0) → c13(BSORT(len(z0), z0), LEN(z0))
K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

<', BUBBLE[ITE][FALSE][ITE], BSORT, LEN, BUBBLE, BUBBLESORT

Compound Symbols:

c2, c5, c6, c7, c9, c11, c13

9.49/2.82
9.49/2.82

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

Removed 1 trailing tuple parts
9.49/2.82
9.49/2.82

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0) 9.49/2.82
+(S(0), z0) → S(z0) 9.49/2.82
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.82
<(0, S(z0)) → True 9.49/2.82
<(z0, 0) → False 9.49/2.82
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.82
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2)) 9.49/2.82
bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2)) 9.49/2.82
bsort(0, z0) → z0 9.49/2.82
len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.82
len(Nil) → 0 9.49/2.82
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.82
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.82
bubblesort(z0) → bsort(len(z0), z0)
Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.82
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.82
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.82
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.82
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.82
BUBBLESORT(z0) → c13(BSORT(len(z0), z0), LEN(z0)) 9.49/2.82
LEN(Cons(z0, z1)) → c9(LEN(z1))
S tuples:

BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.82
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.82
BUBBLESORT(z0) → c13(BSORT(len(z0), z0), LEN(z0)) 9.49/2.82
LEN(Cons(z0, z1)) → c9(LEN(z1))
K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

<', BUBBLE[ITE][FALSE][ITE], BSORT, BUBBLE, BUBBLESORT, LEN

Compound Symbols:

c2, c5, c6, c7, c11, c13, c9

9.49/2.82
9.49/2.82

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

Split RHS of tuples not part of any SCC
9.49/2.82
9.49/2.82

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0) 9.49/2.82
+(S(0), z0) → S(z0) 9.49/2.82
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.82
<(0, S(z0)) → True 9.49/2.82
<(z0, 0) → False 9.49/2.82
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.82
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2)) 9.49/2.82
bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2)) 9.49/2.82
bsort(0, z0) → z0 9.49/2.82
len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.82
len(Nil) → 0 9.49/2.82
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.82
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.82
bubblesort(z0) → bsort(len(z0), z0)
Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.82
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.82
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.82
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.82
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.82
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.82
BUBBLESORT(z0) → c(BSORT(len(z0), z0)) 9.49/2.82
BUBBLESORT(z0) → c(LEN(z0))
S tuples:

BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.82
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.82
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.82
BUBBLESORT(z0) → c(BSORT(len(z0), z0)) 9.49/2.82
BUBBLESORT(z0) → c(LEN(z0))
K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

<', BUBBLE[ITE][FALSE][ITE], BSORT, BUBBLE, LEN, BUBBLESORT

Compound Symbols:

c2, c5, c6, c7, c11, c9, c

9.49/2.82
9.49/2.82

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

BUBBLESORT(z0) → c(LEN(z0))
9.49/2.82
9.49/2.82

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0) 9.49/2.82
+(S(0), z0) → S(z0) 9.49/2.82
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.82
<(0, S(z0)) → True 9.49/2.82
<(z0, 0) → False 9.49/2.82
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.82
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2)) 9.49/2.82
bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2)) 9.49/2.82
bsort(0, z0) → z0 9.49/2.82
len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.82
len(Nil) → 0 9.49/2.82
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.82
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.82
bubblesort(z0) → bsort(len(z0), z0)
Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.82
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
S tuples:

BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

<', BUBBLE[ITE][FALSE][ITE], BSORT, BUBBLE, LEN, BUBBLESORT

Compound Symbols:

c2, c5, c6, c7, c11, c9, c

9.49/2.83
9.49/2.83

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

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

BUBBLESORT(z0) → c(BSORT(len(z0), z0))
9.49/2.83
9.49/2.83

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0) 9.49/2.83
+(S(0), z0) → S(z0) 9.49/2.83
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.83
<(0, S(z0)) → True 9.49/2.83
<(z0, 0) → False 9.49/2.83
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.83
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2)) 9.49/2.83
bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2)) 9.49/2.83
bsort(0, z0) → z0 9.49/2.83
len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.83
len(Nil) → 0 9.49/2.83
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.83
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.83
bubblesort(z0) → bsort(len(z0), z0)
Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
S tuples:

BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1))
K tuples:

BUBBLESORT(z0) → c(BSORT(len(z0), z0))
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

<', BUBBLE[ITE][FALSE][ITE], BSORT, BUBBLE, LEN, BUBBLESORT

Compound Symbols:

c2, c5, c6, c7, c11, c9, c

9.49/2.83
9.49/2.83

(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.

LEN(Cons(z0, z1)) → c9(LEN(z1))
We considered the (Usable) Rules:

len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.83
len(Nil) → 0 9.49/2.83
+(z0, S(0)) → S(z0) 9.49/2.83
+(S(0), z0) → S(z0) 9.49/2.83
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.83
<(0, S(z0)) → True 9.49/2.83
<(z0, 0) → False 9.49/2.83
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.83
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.83
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.83
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
And the Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.49/2.83

POL(+(x1, x2)) = 0    9.49/2.83
POL(0) = 0    9.49/2.83
POL(<(x1, x2)) = 0    9.49/2.83
POL(<'(x1, x2)) = 0    9.49/2.83
POL(BSORT(x1, x2)) = [5]    9.49/2.83
POL(BUBBLE(x1, x2)) = 0    9.49/2.83
POL(BUBBLESORT(x1)) = [5] + [4]x1    9.49/2.83
POL(BUBBLE[ITE][FALSE][ITE](x1, x2, x3)) = 0    9.49/2.83
POL(Cons(x1, x2)) = [1] + x1 + x2    9.49/2.83
POL(False) = [4]    9.49/2.83
POL(LEN(x1)) = x1    9.49/2.83
POL(Nil) = 0    9.49/2.83
POL(S(x1)) = 0    9.49/2.83
POL(True) = 0    9.49/2.83
POL(bubble(x1, x2)) = [1] + [2]x1 + [4]x2    9.49/2.83
POL(bubble[Ite][False][Ite](x1, x2, x3)) = [2]x1 + [2]x2 + [4]x3    9.49/2.83
POL(c(x1)) = x1    9.49/2.83
POL(c11(x1, x2)) = x1 + x2    9.49/2.83
POL(c2(x1)) = x1    9.49/2.83
POL(c5(x1)) = x1    9.49/2.83
POL(c6(x1)) = x1    9.49/2.83
POL(c7(x1, x2)) = x1 + x2    9.49/2.83
POL(c9(x1)) = x1    9.49/2.83
POL(len(x1)) = [2]x1   
9.49/2.83
9.49/2.83

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0) 9.49/2.83
+(S(0), z0) → S(z0) 9.49/2.83
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.83
<(0, S(z0)) → True 9.49/2.83
<(z0, 0) → False 9.49/2.83
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.83
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2)) 9.49/2.83
bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2)) 9.49/2.83
bsort(0, z0) → z0 9.49/2.83
len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.83
len(Nil) → 0 9.49/2.83
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.83
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.83
bubblesort(z0) → bsort(len(z0), z0)
Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
S tuples:

BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
K tuples:

BUBBLESORT(z0) → c(BSORT(len(z0), z0)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1))
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

<', BUBBLE[ITE][FALSE][ITE], BSORT, BUBBLE, LEN, BUBBLESORT

Compound Symbols:

c2, c5, c6, c7, c11, c9, c

9.49/2.83
9.49/2.83

(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.

BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
We considered the (Usable) Rules:

len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.83
len(Nil) → 0 9.49/2.83
+(z0, S(0)) → S(z0) 9.49/2.83
+(S(0), z0) → S(z0) 9.49/2.83
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.83
<(0, S(z0)) → True 9.49/2.83
<(z0, 0) → False 9.49/2.83
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.83
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.83
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.83
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
And the Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.49/2.83

POL(+(x1, x2)) = [4]x1 + x2    9.49/2.83
POL(0) = 0    9.49/2.83
POL(<(x1, x2)) = 0    9.49/2.83
POL(<'(x1, x2)) = 0    9.49/2.83
POL(BSORT(x1, x2)) = [3] + [2]x1    9.49/2.83
POL(BUBBLE(x1, x2)) = 0    9.49/2.83
POL(BUBBLESORT(x1)) = [5] + [4]x1    9.49/2.83
POL(BUBBLE[ITE][FALSE][ITE](x1, x2, x3)) = 0    9.49/2.83
POL(Cons(x1, x2)) = [4] + x2    9.49/2.83
POL(False) = 0    9.49/2.83
POL(LEN(x1)) = [5]x1    9.49/2.83
POL(Nil) = 0    9.49/2.83
POL(S(x1)) = [2] + x1    9.49/2.83
POL(True) = 0    9.49/2.83
POL(bubble(x1, x2)) = 0    9.49/2.83
POL(bubble[Ite][False][Ite](x1, x2, x3)) = [3] + [3]x2 + [3]x3    9.49/2.83
POL(c(x1)) = x1    9.49/2.83
POL(c11(x1, x2)) = x1 + x2    9.49/2.83
POL(c2(x1)) = x1    9.49/2.83
POL(c5(x1)) = x1    9.49/2.83
POL(c6(x1)) = x1    9.49/2.83
POL(c7(x1, x2)) = x1 + x2    9.49/2.83
POL(c9(x1)) = x1    9.49/2.83
POL(len(x1)) = [2]x1   
9.49/2.83
9.49/2.83

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0) 9.49/2.83
+(S(0), z0) → S(z0) 9.49/2.83
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.83
<(0, S(z0)) → True 9.49/2.83
<(z0, 0) → False 9.49/2.83
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.83
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2)) 9.49/2.83
bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2)) 9.49/2.83
bsort(0, z0) → z0 9.49/2.83
len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.83
len(Nil) → 0 9.49/2.83
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.83
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.83
bubblesort(z0) → bsort(len(z0), z0)
Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
S tuples:

BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
K tuples:

BUBBLESORT(z0) → c(BSORT(len(z0), z0)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

<', BUBBLE[ITE][FALSE][ITE], BSORT, BUBBLE, LEN, BUBBLESORT

Compound Symbols:

c2, c5, c6, c7, c11, c9, c

9.49/2.83
9.49/2.83

(15) 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.

BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
We considered the (Usable) Rules:

len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.83
len(Nil) → 0 9.49/2.83
+(z0, S(0)) → S(z0) 9.49/2.83
+(S(0), z0) → S(z0) 9.49/2.83
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.83
<(0, S(z0)) → True 9.49/2.83
<(z0, 0) → False 9.49/2.83
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.83
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.83
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.83
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
And the Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.49/2.83

POL(+(x1, x2)) = x1 + x2    9.49/2.83
POL(0) = 0    9.49/2.83
POL(<(x1, x2)) = 0    9.49/2.83
POL(<'(x1, x2)) = 0    9.49/2.83
POL(BSORT(x1, x2)) = [3] + [2]x1·x2    9.49/2.83
POL(BUBBLE(x1, x2)) = [3] + [3]x2    9.49/2.83
POL(BUBBLESORT(x1)) = [3] + [3]x12    9.49/2.83
POL(BUBBLE[ITE][FALSE][ITE](x1, x2, x3)) = [3]x3    9.49/2.83
POL(Cons(x1, x2)) = [3] + x2    9.49/2.83
POL(False) = 0    9.49/2.83
POL(LEN(x1)) = [3]x1 + [3]x12    9.49/2.83
POL(Nil) = 0    9.49/2.83
POL(S(x1)) = [2] + x1    9.49/2.83
POL(True) = 0    9.49/2.83
POL(bubble(x1, x2)) = [3] + x2    9.49/2.83
POL(bubble[Ite][False][Ite](x1, x2, x3)) = [3] + x3    9.49/2.83
POL(c(x1)) = x1    9.49/2.83
POL(c11(x1, x2)) = x1 + x2    9.49/2.83
POL(c2(x1)) = x1    9.49/2.83
POL(c5(x1)) = x1    9.49/2.83
POL(c6(x1)) = x1    9.49/2.83
POL(c7(x1, x2)) = x1 + x2    9.49/2.83
POL(c9(x1)) = x1    9.49/2.83
POL(len(x1)) = x1   
9.49/2.83
9.49/2.83

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0) 9.49/2.83
+(S(0), z0) → S(z0) 9.49/2.83
<(S(z0), S(z1)) → <(z0, z1) 9.49/2.83
<(0, S(z0)) → True 9.49/2.83
<(z0, 0) → False 9.49/2.83
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2)) 9.49/2.83
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2)) 9.49/2.83
bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2)) 9.49/2.83
bsort(0, z0) → z0 9.49/2.83
len(Cons(z0, z1)) → +(S(0), len(z1)) 9.49/2.83
len(Nil) → 0 9.49/2.83
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 9.49/2.83
bubble(z0, Nil) → Cons(z0, Nil) 9.49/2.83
bubblesort(z0) → bsort(len(z0), z0)
Tuples:

<'(S(z0), S(z1)) → c2(<'(z0, z1)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c5(BUBBLE(z0, z2)) 9.49/2.83
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c6(BUBBLE(z1, z2)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BUBBLESORT(z0) → c(BSORT(len(z0), z0))
S tuples:none
K tuples:

BUBBLESORT(z0) → c(BSORT(len(z0), z0)) 9.49/2.83
LEN(Cons(z0, z1)) → c9(LEN(z1)) 9.49/2.83
BSORT(S(z0), Cons(z1, z2)) → c7(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2)) 9.49/2.83
BUBBLE(z0, Cons(z1, z2)) → c11(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

<', BUBBLE[ITE][FALSE][ITE], BSORT, BUBBLE, LEN, BUBBLESORT

Compound Symbols:

c2, c5, c6, c7, c11, c9, c

9.49/2.83
9.49/2.83

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

The set S is empty
9.49/2.83
9.49/2.83

(18) BOUNDS(O(1), O(1))

9.49/2.83
9.49/2.83
9.49/2.89 EOF