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

0 CpxRelTRS
9.50/2.83 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
9.50/2.83 
↳2 CdtProblem
9.50/2.83 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
9.50/2.83 
↳4 CdtProblem
9.50/2.83 
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
9.50/2.83 
↳6 CdtProblem
9.50/2.83 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
9.50/2.83 
↳8 CdtProblem
9.50/2.83 
↳9 CdtKnowledgeProof (⇔)
9.50/2.83 
↳10 BOUNDS(O(1), O(1))
9.50/2.83
9.50/2.83 9.50/2.83
9.50/2.83
9.50/2.83

(0) Obligation:

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

#less(@x, @y) → #cklt(#compare(@x, @y)) 9.50/2.83
findMin(@l) → findMin#1(@l) 9.50/2.83
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x) 9.50/2.83
findMin#1(nil) → nil 9.50/2.83
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys) 9.50/2.83
findMin#2(nil, @x) → ::(@x, nil) 9.50/2.83
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys)) 9.50/2.83
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys)) 9.50/2.83
minSort(@l) → minSort#1(findMin(@l)) 9.50/2.83
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs)) 9.50/2.83
minSort#1(nil) → nil

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

#cklt(#EQ) → #false 9.50/2.83
#cklt(#GT) → #false 9.50/2.83
#cklt(#LT) → #true 9.50/2.83
#compare(#0, #0) → #EQ 9.50/2.83
#compare(#0, #neg(@y)) → #GT 9.50/2.83
#compare(#0, #pos(@y)) → #LT 9.50/2.83
#compare(#0, #s(@y)) → #LT 9.50/2.83
#compare(#neg(@x), #0) → #LT 9.50/2.83
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x) 9.50/2.83
#compare(#neg(@x), #pos(@y)) → #LT 9.50/2.83
#compare(#pos(@x), #0) → #GT 9.50/2.83
#compare(#pos(@x), #neg(@y)) → #GT 9.50/2.83
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y) 9.50/2.83
#compare(#s(@x), #0) → #GT 9.50/2.85
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Rewrite Strategy: INNERMOST
9.50/2.85
9.50/2.85

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

Relative innermost TRS to CDT Problem.
9.50/2.85
9.50/2.85

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 9.50/2.85
#cklt(#GT) → #false 9.50/2.85
#cklt(#LT) → #true 9.50/2.85
#compare(#0, #0) → #EQ 9.50/2.85
#compare(#0, #neg(z0)) → #GT 9.50/2.85
#compare(#0, #pos(z0)) → #LT 9.50/2.85
#compare(#0, #s(z0)) → #LT 9.50/2.85
#compare(#neg(z0), #0) → #LT 9.50/2.85
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 9.50/2.85
#compare(#neg(z0), #pos(z1)) → #LT 9.50/2.85
#compare(#pos(z0), #0) → #GT 9.50/2.85
#compare(#pos(z0), #neg(z1)) → #GT 9.50/2.85
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 9.50/2.85
#compare(#s(z0), #0) → #GT 9.50/2.85
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 9.50/2.85
#less(z0, z1) → #cklt(#compare(z0, z1)) 9.50/2.85
findMin(z0) → findMin#1(z0) 9.50/2.85
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0) 9.50/2.85
findMin#1(nil) → nil 9.50/2.85
findMin#2(::(z0, z1), z2) → findMin#3(#less(z2, z0), z2, z0, z1) 9.50/2.85
findMin#2(nil, z0) → ::(z0, nil) 9.50/2.85
findMin#3(#false, z0, z1, z2) → ::(z1, ::(z0, z2)) 9.50/2.85
findMin#3(#true, z0, z1, z2) → ::(z0, ::(z1, z2)) 9.50/2.85
minSort(z0) → minSort#1(findMin(z0)) 9.50/2.85
minSort#1(::(z0, z1)) → ::(z0, minSort(z1)) 9.50/2.85
minSort#1(nil) → nil
Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 9.50/2.85
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 9.50/2.85
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 9.50/2.85
#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) 9.50/2.85
FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(FINDMIN#3(#less(z2, z0), z2, z0, z1), #LESS(z2, z0)) 9.50/2.85
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
S tuples:

#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) 9.50/2.85
FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(FINDMIN#3(#less(z2, z0), z2, z0, z1), #LESS(z2, z0)) 9.50/2.85
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
K tuples:none
Defined Rule Symbols:

#less, findMin, findMin#1, findMin#2, findMin#3, minSort, minSort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, #LESS, FINDMIN, FINDMIN#1, FINDMIN#2, MINSORT, MINSORT#1

Compound Symbols:

c8, c12, c14, c15, c16, c17, c19, c23, c24

9.50/2.85
9.50/2.85

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

Removed 2 trailing tuple parts
9.50/2.85
9.50/2.85

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 9.50/2.85
#cklt(#GT) → #false 9.50/2.85
#cklt(#LT) → #true 9.50/2.85
#compare(#0, #0) → #EQ 9.50/2.85
#compare(#0, #neg(z0)) → #GT 9.50/2.85
#compare(#0, #pos(z0)) → #LT 9.50/2.85
#compare(#0, #s(z0)) → #LT 9.50/2.85
#compare(#neg(z0), #0) → #LT 9.50/2.85
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 9.50/2.85
#compare(#neg(z0), #pos(z1)) → #LT 9.50/2.85
#compare(#pos(z0), #0) → #GT 9.50/2.85
#compare(#pos(z0), #neg(z1)) → #GT 9.50/2.85
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 9.50/2.85
#compare(#s(z0), #0) → #GT 9.50/2.85
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 9.50/2.85
#less(z0, z1) → #cklt(#compare(z0, z1)) 9.50/2.85
findMin(z0) → findMin#1(z0) 9.50/2.85
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0) 9.50/2.85
findMin#1(nil) → nil 9.50/2.85
findMin#2(::(z0, z1), z2) → findMin#3(#less(z2, z0), z2, z0, z1) 9.50/2.85
findMin#2(nil, z0) → ::(z0, nil) 9.50/2.85
findMin#3(#false, z0, z1, z2) → ::(z1, ::(z0, z2)) 9.50/2.85
findMin#3(#true, z0, z1, z2) → ::(z0, ::(z1, z2)) 9.50/2.85
minSort(z0) → minSort#1(findMin(z0)) 9.50/2.85
minSort#1(::(z0, z1)) → ::(z0, minSort(z1)) 9.50/2.85
minSort#1(nil) → nil
Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 9.50/2.85
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 9.50/2.85
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
S tuples:

FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
K tuples:none
Defined Rule Symbols:

#less, findMin, findMin#1, findMin#2, findMin#3, minSort, minSort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, FINDMIN, FINDMIN#1, MINSORT, MINSORT#1, #LESS, FINDMIN#2

Compound Symbols:

c8, c12, c14, c16, c17, c23, c24, c15, c19

9.50/2.85
9.50/2.85

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

MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
We considered the (Usable) Rules:

findMin(z0) → findMin#1(z0) 9.50/2.85
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0) 9.50/2.85
findMin#1(nil) → nil 9.50/2.85
findMin#2(::(z0, z1), z2) → findMin#3(#less(z2, z0), z2, z0, z1) 9.50/2.85
findMin#2(nil, z0) → ::(z0, nil) 9.50/2.85
#less(z0, z1) → #cklt(#compare(z0, z1)) 9.50/2.85
findMin#3(#false, z0, z1, z2) → ::(z1, ::(z0, z2)) 9.50/2.85
findMin#3(#true, z0, z1, z2) → ::(z0, ::(z1, z2)) 9.50/2.85
#compare(#0, #0) → #EQ 9.50/2.85
#compare(#0, #neg(z0)) → #GT 9.50/2.85
#compare(#0, #pos(z0)) → #LT 9.50/2.85
#compare(#0, #s(z0)) → #LT 9.50/2.85
#compare(#neg(z0), #0) → #LT 9.50/2.85
#compare(#neg(z0), #pos(z1)) → #LT 9.50/2.85
#compare(#pos(z0), #0) → #GT 9.50/2.85
#compare(#pos(z0), #neg(z1)) → #GT 9.50/2.85
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 9.50/2.85
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 9.50/2.85
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 9.50/2.85
#compare(#s(z0), #0) → #GT 9.50/2.85
#cklt(#EQ) → #false 9.50/2.85
#cklt(#GT) → #false 9.50/2.85
#cklt(#LT) → #true
And the Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 9.50/2.85
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 9.50/2.85
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.50/2.85

POL(#0) = 0    9.50/2.85
POL(#COMPARE(x1, x2)) = 0    9.50/2.85
POL(#EQ) = 0    9.50/2.85
POL(#GT) = 0    9.50/2.85
POL(#LESS(x1, x2)) = 0    9.50/2.85
POL(#LT) = 0    9.50/2.85
POL(#cklt(x1)) = [3]    9.50/2.85
POL(#compare(x1, x2)) = 0    9.50/2.85
POL(#false) = 0    9.50/2.85
POL(#less(x1, x2)) = 0    9.50/2.85
POL(#neg(x1)) = 0    9.50/2.85
POL(#pos(x1)) = x1    9.50/2.85
POL(#s(x1)) = x1    9.50/2.85
POL(#true) = 0    9.50/2.85
POL(::(x1, x2)) = [1] + x2    9.50/2.85
POL(FINDMIN(x1)) = 0    9.50/2.85
POL(FINDMIN#1(x1)) = 0    9.50/2.85
POL(FINDMIN#2(x1, x2)) = 0    9.50/2.85
POL(MINSORT(x1)) = [1] + [2]x1    9.50/2.85
POL(MINSORT#1(x1)) = [2]x1    9.50/2.85
POL(c12(x1)) = x1    9.50/2.85
POL(c14(x1)) = x1    9.50/2.85
POL(c15(x1)) = x1    9.50/2.85
POL(c16(x1)) = x1    9.50/2.85
POL(c17(x1, x2)) = x1 + x2    9.50/2.85
POL(c19(x1)) = x1    9.50/2.85
POL(c23(x1, x2)) = x1 + x2    9.50/2.85
POL(c24(x1)) = x1    9.50/2.85
POL(c8(x1)) = x1    9.50/2.85
POL(findMin(x1)) = x1    9.50/2.85
POL(findMin#1(x1)) = x1    9.50/2.85
POL(findMin#2(x1, x2)) = [1] + x1    9.50/2.85
POL(findMin#3(x1, x2, x3, x4)) = [2] + x4    9.50/2.85
POL(nil) = 0   
9.50/2.85
9.50/2.85

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 9.50/2.85
#cklt(#GT) → #false 9.50/2.85
#cklt(#LT) → #true 9.50/2.85
#compare(#0, #0) → #EQ 9.50/2.85
#compare(#0, #neg(z0)) → #GT 9.50/2.85
#compare(#0, #pos(z0)) → #LT 9.50/2.85
#compare(#0, #s(z0)) → #LT 9.50/2.85
#compare(#neg(z0), #0) → #LT 9.50/2.85
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 9.50/2.85
#compare(#neg(z0), #pos(z1)) → #LT 9.50/2.85
#compare(#pos(z0), #0) → #GT 9.50/2.85
#compare(#pos(z0), #neg(z1)) → #GT 9.50/2.85
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 9.50/2.85
#compare(#s(z0), #0) → #GT 9.50/2.85
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 9.50/2.85
#less(z0, z1) → #cklt(#compare(z0, z1)) 9.50/2.85
findMin(z0) → findMin#1(z0) 9.50/2.85
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0) 9.50/2.85
findMin#1(nil) → nil 9.50/2.85
findMin#2(::(z0, z1), z2) → findMin#3(#less(z2, z0), z2, z0, z1) 9.50/2.85
findMin#2(nil, z0) → ::(z0, nil) 9.50/2.85
findMin#3(#false, z0, z1, z2) → ::(z1, ::(z0, z2)) 9.50/2.85
findMin#3(#true, z0, z1, z2) → ::(z0, ::(z1, z2)) 9.50/2.85
minSort(z0) → minSort#1(findMin(z0)) 9.50/2.85
minSort#1(::(z0, z1)) → ::(z0, minSort(z1)) 9.50/2.85
minSort#1(nil) → nil
Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 9.50/2.85
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 9.50/2.85
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
S tuples:

FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
K tuples:

MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
Defined Rule Symbols:

#less, findMin, findMin#1, findMin#2, findMin#3, minSort, minSort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, FINDMIN, FINDMIN#1, MINSORT, MINSORT#1, #LESS, FINDMIN#2

Compound Symbols:

c8, c12, c14, c16, c17, c23, c24, c15, c19

9.50/2.85
9.50/2.85

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

FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
We considered the (Usable) Rules:

findMin(z0) → findMin#1(z0) 9.50/2.85
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0) 9.50/2.85
findMin#1(nil) → nil 9.50/2.85
findMin#2(::(z0, z1), z2) → findMin#3(#less(z2, z0), z2, z0, z1) 9.50/2.85
findMin#2(nil, z0) → ::(z0, nil) 9.50/2.85
#less(z0, z1) → #cklt(#compare(z0, z1)) 9.50/2.85
findMin#3(#false, z0, z1, z2) → ::(z1, ::(z0, z2)) 9.50/2.85
findMin#3(#true, z0, z1, z2) → ::(z0, ::(z1, z2)) 9.50/2.85
#compare(#0, #0) → #EQ 9.50/2.85
#compare(#0, #neg(z0)) → #GT 9.50/2.85
#compare(#0, #pos(z0)) → #LT 9.50/2.85
#compare(#0, #s(z0)) → #LT 9.50/2.85
#compare(#neg(z0), #0) → #LT 9.50/2.85
#compare(#neg(z0), #pos(z1)) → #LT 9.50/2.85
#compare(#pos(z0), #0) → #GT 9.50/2.85
#compare(#pos(z0), #neg(z1)) → #GT 9.50/2.85
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 9.50/2.85
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 9.50/2.85
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 9.50/2.85
#compare(#s(z0), #0) → #GT 9.50/2.85
#cklt(#EQ) → #false 9.50/2.85
#cklt(#GT) → #false 9.50/2.85
#cklt(#LT) → #true
And the Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 9.50/2.85
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 9.50/2.85
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.50/2.85

POL(#0) = 0    9.50/2.85
POL(#COMPARE(x1, x2)) = 0    9.50/2.85
POL(#EQ) = 0    9.50/2.85
POL(#GT) = 0    9.50/2.85
POL(#LESS(x1, x2)) = 0    9.50/2.85
POL(#LT) = 0    9.50/2.85
POL(#cklt(x1)) = [3]    9.50/2.85
POL(#compare(x1, x2)) = [3]x22    9.50/2.85
POL(#false) = 0    9.50/2.85
POL(#less(x1, x2)) = x22    9.50/2.85
POL(#neg(x1)) = 0    9.50/2.85
POL(#pos(x1)) = 0    9.50/2.85
POL(#s(x1)) = 0    9.50/2.85
POL(#true) = 0    9.50/2.85
POL(::(x1, x2)) = [1] + x2    9.50/2.85
POL(FINDMIN(x1)) = [2]x1    9.50/2.85
POL(FINDMIN#1(x1)) = [2]x1    9.50/2.85
POL(FINDMIN#2(x1, x2)) = 0    9.50/2.85
POL(MINSORT(x1)) = [2] + [2]x1 + [2]x12    9.50/2.85
POL(MINSORT#1(x1)) = [2]x12    9.50/2.85
POL(c12(x1)) = x1    9.50/2.85
POL(c14(x1)) = x1    9.50/2.85
POL(c15(x1)) = x1    9.50/2.85
POL(c16(x1)) = x1    9.50/2.85
POL(c17(x1, x2)) = x1 + x2    9.50/2.85
POL(c19(x1)) = x1    9.50/2.85
POL(c23(x1, x2)) = x1 + x2    9.50/2.85
POL(c24(x1)) = x1    9.50/2.85
POL(c8(x1)) = x1    9.50/2.85
POL(findMin(x1)) = x1    9.50/2.85
POL(findMin#1(x1)) = x1    9.50/2.85
POL(findMin#2(x1, x2)) = [1] + x1    9.50/2.85
POL(findMin#3(x1, x2, x3, x4)) = [2] + x4    9.50/2.85
POL(nil) = 0   
9.50/2.85
9.50/2.85

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 9.50/2.85
#cklt(#GT) → #false 9.50/2.85
#cklt(#LT) → #true 9.50/2.85
#compare(#0, #0) → #EQ 9.50/2.85
#compare(#0, #neg(z0)) → #GT 9.50/2.85
#compare(#0, #pos(z0)) → #LT 9.50/2.85
#compare(#0, #s(z0)) → #LT 9.50/2.85
#compare(#neg(z0), #0) → #LT 9.50/2.85
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 9.50/2.85
#compare(#neg(z0), #pos(z1)) → #LT 9.50/2.85
#compare(#pos(z0), #0) → #GT 9.50/2.85
#compare(#pos(z0), #neg(z1)) → #GT 9.50/2.85
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 9.50/2.85
#compare(#s(z0), #0) → #GT 9.50/2.85
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 9.50/2.85
#less(z0, z1) → #cklt(#compare(z0, z1)) 9.50/2.85
findMin(z0) → findMin#1(z0) 9.50/2.85
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0) 9.50/2.85
findMin#1(nil) → nil 9.50/2.85
findMin#2(::(z0, z1), z2) → findMin#3(#less(z2, z0), z2, z0, z1) 9.50/2.85
findMin#2(nil, z0) → ::(z0, nil) 9.50/2.85
findMin#3(#false, z0, z1, z2) → ::(z1, ::(z0, z2)) 9.50/2.85
findMin#3(#true, z0, z1, z2) → ::(z0, ::(z1, z2)) 9.50/2.85
minSort(z0) → minSort#1(findMin(z0)) 9.50/2.85
minSort#1(::(z0, z1)) → ::(z0, minSort(z1)) 9.50/2.85
minSort#1(nil) → nil
Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 9.50/2.85
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 9.50/2.85
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
S tuples:

FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
K tuples:

MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0)) 9.50/2.85
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
Defined Rule Symbols:

#less, findMin, findMin#1, findMin#2, findMin#3, minSort, minSort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, FINDMIN, FINDMIN#1, MINSORT, MINSORT#1, #LESS, FINDMIN#2

Compound Symbols:

c8, c12, c14, c16, c17, c23, c24, c15, c19

9.50/2.85
9.50/2.85

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

FINDMIN(z0) → c16(FINDMIN#1(z0)) 9.50/2.85
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0)) 9.50/2.85
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1)) 9.50/2.85
#LESS(z0, z1) → c15(#COMPARE(z0, z1))
Now S is empty
9.50/2.85
9.50/2.85

(10) BOUNDS(O(1), O(1))

9.50/2.85
9.50/2.85
9.77/2.91 EOF