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

0 CpxRelTRS
30.51/9.94 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
30.51/9.94 
↳2 CdtProblem
30.51/9.94 
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
30.51/9.94 
↳4 CdtProblem
30.51/9.94 
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
30.51/9.94 
↳6 CdtProblem
30.51/9.94 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
30.51/9.94 
↳8 CdtProblem
30.51/9.94 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
30.51/9.94 
↳10 CdtProblem
30.51/9.94 
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))
30.51/9.94 
↳12 BOUNDS(O(1), O(1))
30.51/9.94
30.51/9.94 30.51/9.94
30.51/9.94
30.51/9.94

(0) Obligation:

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

qs(x', Cons(x, xs)) → app(Cons(x, Nil), Cons(x', quicksort(xs))) 30.51/9.94
quicksort(Cons(x, Cons(x', xs))) → qs(x, part(x, Cons(x', xs), Nil, Nil)) 30.51/9.94
quicksort(Cons(x, Nil)) → Cons(x, Nil) 30.51/9.94
quicksort(Nil) → Nil 30.51/9.94
part(x', Cons(x, xs), xs1, xs2) → part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 30.51/9.94
part(x, Nil, xs1, xs2) → app(xs1, xs2) 30.51/9.94
app(Cons(x, xs), ys) → Cons(x, app(xs, ys)) 30.51/9.94
app(Nil, ys) → ys 30.51/9.94
notEmpty(Cons(x, xs)) → True 30.51/9.94
notEmpty(Nil) → False

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

<(S(x), S(y)) → <(x, y) 30.51/9.94
<(0, S(y)) → True 30.51/9.94
<(x, 0) → False 30.51/9.94
>(S(x), S(y)) → >(x, y) 30.51/9.94
>(0, y) → False 30.51/9.94
>(S(x), 0) → True 30.51/9.94
part[Ite][True][Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, Cons(x, xs1), xs2) 30.51/9.94
part[Ite][True][Ite](False, x', Cons(x, xs), xs1, xs2) → part[Ite][True][Ite][False][Ite](<(x', x), x', Cons(x, xs), xs1, xs2)

Rewrite Strategy: INNERMOST
30.51/9.97
30.51/9.97

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

Relative innermost TRS to CDT Problem.
30.51/9.97
30.51/9.97

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 30.51/9.97
<(0, S(z0)) → True 30.51/9.97
<(z0, 0) → False 30.51/9.97
>(S(z0), S(z1)) → >(z0, z1) 30.51/9.97
>(0, z0) → False 30.51/9.97
>(S(z0), 0) → True 30.51/9.97
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.97
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.97
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2))) 30.51/9.97
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.97
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.97
quicksort(Nil) → Nil 30.51/9.97
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.97
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.97
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.97
app(Nil, z0) → z0 30.51/9.97
notEmpty(Cons(z0, z1)) → True 30.51/9.97
notEmpty(Nil) → False
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.97
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.97
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.97
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.97
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.97
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.97
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.97
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.97
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.97
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.97
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.97
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.97
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
K tuples:none
Defined Rule Symbols:

qs, quicksort, part, app, notEmpty, <, >, part[Ite][True][Ite]

Defined Pair Symbols:

<', >', PART[ITE][TRUE][ITE], QS, QUICKSORT, PART, APP

Compound Symbols:

c, c3, c6, c7, c8, c9, c12, c13, c14

30.51/9.97
30.51/9.97

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

QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.97
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil))
We considered the (Usable) Rules:

>(S(z0), S(z1)) → >(z0, z1) 30.51/9.97
>(0, z0) → False 30.51/9.97
>(S(z0), 0) → True 30.51/9.97
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.97
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.97
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.97
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.97
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.97
app(Nil, z0) → z0 30.51/9.97
<(S(z0), S(z1)) → <(z0, z1) 30.51/9.97
<(0, S(z0)) → True 30.51/9.97
<(z0, 0) → False 30.51/9.97
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.97
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.97
quicksort(Nil) → Nil 30.51/9.97
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2)))
And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.97
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.97
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.97
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.97
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.97
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.97
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.97
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.97
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 30.51/9.97

POL(0) = [1]    30.51/9.97
POL(<(x1, x2)) = [4] + x1 + x2    30.51/9.97
POL(<'(x1, x2)) = 0    30.51/9.97
POL(>(x1, x2)) = 0    30.51/9.97
POL(>'(x1, x2)) = 0    30.51/9.97
POL(APP(x1, x2)) = 0    30.51/9.97
POL(Cons(x1, x2)) = [1] + x2    30.51/9.97
POL(False) = 0    30.51/9.97
POL(Nil) = 0    30.51/9.97
POL(PART(x1, x2, x3, x4)) = [2]x4    30.51/9.97
POL(PART[ITE][TRUE][ITE](x1, x2, x3, x4, x5)) = [2]x5    30.51/9.97
POL(QS(x1, x2)) = [4]x2    30.51/9.97
POL(QUICKSORT(x1)) = [4]x1    30.51/9.97
POL(S(x1)) = [1] + x1    30.51/9.97
POL(True) = 0    30.51/9.97
POL(app(x1, x2)) = x1 + [4]x2    30.51/9.97
POL(c(x1)) = x1    30.51/9.97
POL(c12(x1, x2)) = x1 + x2    30.51/9.97
POL(c13(x1)) = x1    30.51/9.97
POL(c14(x1)) = x1    30.51/9.97
POL(c3(x1)) = x1    30.51/9.97
POL(c6(x1)) = x1    30.51/9.97
POL(c7(x1)) = x1    30.51/9.97
POL(c8(x1, x2)) = x1 + x2    30.51/9.97
POL(c9(x1, x2)) = x1 + x2    30.51/9.97
POL(part(x1, x2, x3, x4)) = x2 + x3 + [4]x4    30.51/9.97
POL(part[Ite][True][Ite](x1, x2, x3, x4, x5)) = x3 + x4 + [4]x5    30.51/9.97
POL(part[Ite][True][Ite][False][Ite](x1, x2, x3, x4, x5)) = [1] + x4    30.51/9.97
POL(qs(x1, x2)) = [3] + [3]x1    30.51/9.97
POL(quicksort(x1)) = 0   
30.51/9.97
30.51/9.97

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 30.51/9.97
<(0, S(z0)) → True 30.51/9.97
<(z0, 0) → False 30.51/9.97
>(S(z0), S(z1)) → >(z0, z1) 30.51/9.97
>(0, z0) → False 30.51/9.97
>(S(z0), 0) → True 30.51/9.97
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.97
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.97
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2))) 30.51/9.97
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.98
quicksort(Nil) → Nil 30.51/9.98
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.98
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.98
app(Nil, z0) → z0 30.51/9.98
notEmpty(Cons(z0, z1)) → True 30.51/9.98
notEmpty(Nil) → False
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.98
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.98
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.98
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.98
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
K tuples:

QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil))
Defined Rule Symbols:

qs, quicksort, part, app, notEmpty, <, >, part[Ite][True][Ite]

Defined Pair Symbols:

<', >', PART[ITE][TRUE][ITE], QS, QUICKSORT, PART, APP

Compound Symbols:

c, c3, c6, c7, c8, c9, c12, c13, c14

30.51/9.98
30.51/9.98

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

PART(z0, Nil, z1, z2) → c13(APP(z1, z2))
We considered the (Usable) Rules:

>(S(z0), S(z1)) → >(z0, z1) 30.51/9.98
>(0, z0) → False 30.51/9.98
>(S(z0), 0) → True 30.51/9.98
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.98
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.98
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.98
app(Nil, z0) → z0 30.51/9.98
<(S(z0), S(z1)) → <(z0, z1) 30.51/9.98
<(0, S(z0)) → True 30.51/9.98
<(z0, 0) → False 30.51/9.98
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.98
quicksort(Nil) → Nil 30.51/9.98
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2)))
And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.98
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.98
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.98
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.98
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 30.51/9.98

POL(0) = 0    30.51/9.98
POL(<(x1, x2)) = [3] + [3]x1 + [5]x2    30.51/9.98
POL(<'(x1, x2)) = [1]    30.51/9.98
POL(>(x1, x2)) = 0    30.51/9.98
POL(>'(x1, x2)) = 0    30.51/9.98
POL(APP(x1, x2)) = 0    30.51/9.98
POL(Cons(x1, x2)) = [1] + x2    30.51/9.98
POL(False) = 0    30.51/9.98
POL(Nil) = 0    30.51/9.98
POL(PART(x1, x2, x3, x4)) = [1]    30.51/9.98
POL(PART[ITE][TRUE][ITE](x1, x2, x3, x4, x5)) = [1]    30.51/9.98
POL(QS(x1, x2)) = [4] + [4]x2    30.51/9.98
POL(QUICKSORT(x1)) = [1] + [4]x1    30.51/9.98
POL(S(x1)) = x1    30.51/9.98
POL(True) = 0    30.51/9.98
POL(app(x1, x2)) = x1 + x2    30.51/9.98
POL(c(x1)) = x1    30.51/9.98
POL(c12(x1, x2)) = x1 + x2    30.51/9.98
POL(c13(x1)) = x1    30.51/9.98
POL(c14(x1)) = x1    30.51/9.98
POL(c3(x1)) = x1    30.51/9.98
POL(c6(x1)) = x1    30.51/9.98
POL(c7(x1)) = x1    30.51/9.98
POL(c8(x1, x2)) = x1 + x2    30.51/9.98
POL(c9(x1, x2)) = x1 + x2    30.51/9.98
POL(part(x1, x2, x3, x4)) = x2 + x3 + [4]x4    30.51/9.98
POL(part[Ite][True][Ite](x1, x2, x3, x4, x5)) = x3 + x4 + [4]x5    30.51/9.98
POL(part[Ite][True][Ite][False][Ite](x1, x2, x3, x4, x5)) = [1] + x4 + x5    30.51/9.98
POL(qs(x1, x2)) = [3] + [3]x1    30.51/9.98
POL(quicksort(x1)) = 0   
30.51/9.98
30.51/9.98

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 30.51/9.98
<(0, S(z0)) → True 30.51/9.98
<(z0, 0) → False 30.51/9.98
>(S(z0), S(z1)) → >(z0, z1) 30.51/9.98
>(0, z0) → False 30.51/9.98
>(S(z0), 0) → True 30.51/9.98
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.98
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2))) 30.51/9.98
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.98
quicksort(Nil) → Nil 30.51/9.98
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.98
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.98
app(Nil, z0) → z0 30.51/9.98
notEmpty(Cons(z0, z1)) → True 30.51/9.98
notEmpty(Nil) → False
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.98
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.98
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.98
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.98
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
K tuples:

QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2))
Defined Rule Symbols:

qs, quicksort, part, app, notEmpty, <, >, part[Ite][True][Ite]

Defined Pair Symbols:

<', >', PART[ITE][TRUE][ITE], QS, QUICKSORT, PART, APP

Compound Symbols:

c, c3, c6, c7, c8, c9, c12, c13, c14

30.51/9.98
30.51/9.98

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

PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
We considered the (Usable) Rules:

>(S(z0), S(z1)) → >(z0, z1) 30.51/9.98
>(0, z0) → False 30.51/9.98
>(S(z0), 0) → True 30.51/9.98
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.98
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.98
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.98
app(Nil, z0) → z0 30.51/9.98
<(S(z0), S(z1)) → <(z0, z1) 30.51/9.98
<(0, S(z0)) → True 30.51/9.98
<(z0, 0) → False 30.51/9.98
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.98
quicksort(Nil) → Nil 30.51/9.98
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2)))
And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.98
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.98
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.98
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.98
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 30.51/9.98

POL(0) = 0    30.51/9.98
POL(<(x1, x2)) = [3]    30.51/9.98
POL(<'(x1, x2)) = [3]    30.51/9.98
POL(>(x1, x2)) = 0    30.51/9.98
POL(>'(x1, x2)) = 0    30.51/9.98
POL(APP(x1, x2)) = [2] + [2]x2    30.51/9.98
POL(Cons(x1, x2)) = [1] + x2    30.51/9.98
POL(False) = 0    30.51/9.98
POL(Nil) = 0    30.51/9.98
POL(PART(x1, x2, x3, x4)) = [3] + [2]x2 + [2]x4 + [3]x1·x4    30.51/9.98
POL(PART[ITE][TRUE][ITE](x1, x2, x3, x4, x5)) = [1] + [2]x3 + [2]x5 + [3]x2·x5    30.51/9.98
POL(QS(x1, x2)) = [3] + [2]x22    30.51/9.98
POL(QUICKSORT(x1)) = [2]x1 + [2]x12    30.51/9.98
POL(S(x1)) = 0    30.51/9.98
POL(True) = 0    30.51/9.98
POL(app(x1, x2)) = x1 + x2    30.51/9.98
POL(c(x1)) = x1    30.51/9.98
POL(c12(x1, x2)) = x1 + x2    30.51/9.98
POL(c13(x1)) = x1    30.51/9.98
POL(c14(x1)) = x1    30.51/9.98
POL(c3(x1)) = x1    30.51/9.98
POL(c6(x1)) = x1    30.51/9.98
POL(c7(x1)) = x1    30.51/9.98
POL(c8(x1, x2)) = x1 + x2    30.51/9.98
POL(c9(x1, x2)) = x1 + x2    30.51/9.98
POL(part(x1, x2, x3, x4)) = x2 + x3 + x4    30.51/9.98
POL(part[Ite][True][Ite](x1, x2, x3, x4, x5)) = x3 + x4 + x5    30.51/9.98
POL(part[Ite][True][Ite][False][Ite](x1, x2, x3, x4, x5)) = x4 + x5    30.51/9.98
POL(qs(x1, x2)) = [1] + x2    30.51/9.98
POL(quicksort(x1)) = x1   
30.51/9.98
30.51/9.98

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 30.51/9.98
<(0, S(z0)) → True 30.51/9.98
<(z0, 0) → False 30.51/9.98
>(S(z0), S(z1)) → >(z0, z1) 30.51/9.98
>(0, z0) → False 30.51/9.98
>(S(z0), 0) → True 30.51/9.98
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.98
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2))) 30.51/9.98
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.98
quicksort(Nil) → Nil 30.51/9.98
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.98
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.98
app(Nil, z0) → z0 30.51/9.98
notEmpty(Cons(z0, z1)) → True 30.51/9.98
notEmpty(Nil) → False
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.98
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.98
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.98
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.98
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:

APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
K tuples:

QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1))
Defined Rule Symbols:

qs, quicksort, part, app, notEmpty, <, >, part[Ite][True][Ite]

Defined Pair Symbols:

<', >', PART[ITE][TRUE][ITE], QS, QUICKSORT, PART, APP

Compound Symbols:

c, c3, c6, c7, c8, c9, c12, c13, c14

30.51/9.98
30.51/9.98

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

APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
We considered the (Usable) Rules:

>(S(z0), S(z1)) → >(z0, z1) 30.51/9.98
>(0, z0) → False 30.51/9.98
>(S(z0), 0) → True 30.51/9.98
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.98
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.98
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.98
app(Nil, z0) → z0 30.51/9.98
<(S(z0), S(z1)) → <(z0, z1) 30.51/9.98
<(0, S(z0)) → True 30.51/9.98
<(z0, 0) → False 30.51/9.98
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.98
quicksort(Nil) → Nil 30.51/9.98
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2)))
And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.98
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.98
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.98
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.98
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 30.51/9.98

POL(0) = 0    30.51/9.98
POL(<(x1, x2)) = [3]    30.51/9.98
POL(<'(x1, x2)) = [2]    30.51/9.98
POL(>(x1, x2)) = 0    30.51/9.98
POL(>'(x1, x2)) = [2]    30.51/9.98
POL(APP(x1, x2)) = [2]x1    30.51/9.98
POL(Cons(x1, x2)) = [2] + x2    30.51/9.98
POL(False) = 0    30.51/9.98
POL(Nil) = 0    30.51/9.98
POL(PART(x1, x2, x3, x4)) = [2] + [3]x2 + [2]x3 + [3]x1·x4    30.51/9.98
POL(PART[ITE][TRUE][ITE](x1, x2, x3, x4, x5)) = [3]x3 + [2]x4 + [3]x2·x5    30.51/9.98
POL(QS(x1, x2)) = x22    30.51/9.98
POL(QUICKSORT(x1)) = x12    30.51/9.98
POL(S(x1)) = 0    30.51/9.98
POL(True) = 0    30.51/9.98
POL(app(x1, x2)) = x1 + x2    30.51/9.98
POL(c(x1)) = x1    30.51/9.98
POL(c12(x1, x2)) = x1 + x2    30.51/9.98
POL(c13(x1)) = x1    30.51/9.98
POL(c14(x1)) = x1    30.51/9.98
POL(c3(x1)) = x1    30.51/9.98
POL(c6(x1)) = x1    30.51/9.98
POL(c7(x1)) = x1    30.51/9.98
POL(c8(x1, x2)) = x1 + x2    30.51/9.98
POL(c9(x1, x2)) = x1 + x2    30.51/9.98
POL(part(x1, x2, x3, x4)) = x2 + x3 + x4    30.51/9.98
POL(part[Ite][True][Ite](x1, x2, x3, x4, x5)) = x3 + x4 + x5    30.51/9.98
POL(part[Ite][True][Ite][False][Ite](x1, x2, x3, x4, x5)) = x4 + x5    30.51/9.98
POL(qs(x1, x2)) = [3] + [3]x1 + [3]x12    30.51/9.98
POL(quicksort(x1)) = 0   
30.51/9.98
30.51/9.98

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 30.51/9.98
<(0, S(z0)) → True 30.51/9.98
<(z0, 0) → False 30.51/9.98
>(S(z0), S(z1)) → >(z0, z1) 30.51/9.98
>(0, z0) → False 30.51/9.98
>(S(z0), 0) → True 30.51/9.98
part[Ite][True][Ite](True, z0, Cons(z1, z2), z3, z4) → part(z0, z2, Cons(z1, z3), z4) 30.51/9.98
part[Ite][True][Ite](False, z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
qs(z0, Cons(z1, z2)) → app(Cons(z1, Nil), Cons(z0, quicksort(z2))) 30.51/9.98
quicksort(Cons(z0, Cons(z1, z2))) → qs(z0, part(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
quicksort(Cons(z0, Nil)) → Cons(z0, Nil) 30.51/9.98
quicksort(Nil) → Nil 30.51/9.98
part(z0, Cons(z1, z2), z3, z4) → part[Ite][True][Ite](>(z0, z1), z0, Cons(z1, z2), z3, z4) 30.51/9.98
part(z0, Nil, z1, z2) → app(z1, z2) 30.51/9.98
app(Cons(z0, z1), z2) → Cons(z0, app(z1, z2)) 30.51/9.98
app(Nil, z0) → z0 30.51/9.98
notEmpty(Cons(z0, z1)) → True 30.51/9.98
notEmpty(Nil) → False
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 30.51/9.98
>'(S(z0), S(z1)) → c3(>'(z0, z1)) 30.51/9.98
PART[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3, z4) → c6(PART(z0, z2, Cons(z1, z3), z4)) 30.51/9.98
PART[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3, z4) → c7(<'(z0, z1)) 30.51/9.98
QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
S tuples:none
K tuples:

QS(z0, Cons(z1, z2)) → c8(APP(Cons(z1, Nil), Cons(z0, quicksort(z2))), QUICKSORT(z2)) 30.51/9.98
QUICKSORT(Cons(z0, Cons(z1, z2))) → c9(QS(z0, part(z0, Cons(z1, z2), Nil, Nil)), PART(z0, Cons(z1, z2), Nil, Nil)) 30.51/9.98
PART(z0, Nil, z1, z2) → c13(APP(z1, z2)) 30.51/9.98
PART(z0, Cons(z1, z2), z3, z4) → c12(PART[ITE][TRUE][ITE](>(z0, z1), z0, Cons(z1, z2), z3, z4), >'(z0, z1)) 30.51/9.98
APP(Cons(z0, z1), z2) → c14(APP(z1, z2))
Defined Rule Symbols:

qs, quicksort, part, app, notEmpty, <, >, part[Ite][True][Ite]

Defined Pair Symbols:

<', >', PART[ITE][TRUE][ITE], QS, QUICKSORT, PART, APP

Compound Symbols:

c, c3, c6, c7, c8, c9, c12, c13, c14

30.51/9.98
30.51/9.98

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

The set S is empty
30.51/9.98
30.51/9.98

(12) BOUNDS(O(1), O(1))

30.51/9.98
30.51/9.98
30.81/10.02 EOF