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

0 CpxRelTRS
↳1 CpxTrsToCdtProof (UPPER BOUND(ID), 0 ms)
↳2 CdtProblem
↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CdtProblem
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtUsableRulesProof (⇔, 0 ms)
↳8 CdtProblem
↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 339 ms)
↳10 CdtProblem
↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳12 CdtProblem
↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 369 ms)
↳14 CdtProblem
↳15 CdtKnowledgeProof (⇔, 0 ms)
↳16 BOUNDS(1, 1)

(0) Obligation:

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

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

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

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

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

#CKLT(#EQ) → c
#CKLT(#GT) → c1
#CKLT(#LT) → c2
#COMPARE(#0, #0) → c3
#COMPARE(#0, #neg(z0)) → c4
#COMPARE(#0, #pos(z0)) → c5
#COMPARE(#0, #s(z0)) → c6
#COMPARE(#neg(z0), #0) → c7
#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) → c9
#COMPARE(#pos(z0), #0) → c10
#COMPARE(#pos(z0), #neg(z1)) → c11
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) → c13
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1))
#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
FINDMIN(z0) → c16(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN#1(nil) → c18
FINDMIN#2(::(z0, z1), z2) → c19(FINDMIN#3(#less(z2, z0), z2, z0, z1), #LESS(z2, z0))
FINDMIN#2(nil, z0) → c20
FINDMIN#3(#false, z0, z1, z2) → c21
FINDMIN#3(#true, z0, z1, z2) → c22
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
MINSORT#1(nil) → c25
S tuples:

#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
FINDMIN(z0) → c16(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN#1(nil) → c18
FINDMIN#2(::(z0, z1), z2) → c19(FINDMIN#3(#less(z2, z0), z2, z0, z1), #LESS(z2, z0))
FINDMIN#2(nil, z0) → c20
FINDMIN#3(#false, z0, z1, z2) → c21
FINDMIN#3(#true, z0, z1, z2) → c22
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
MINSORT#1(nil) → c25
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

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

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

Removed 17 trailing nodes:

FINDMIN#2(nil, z0) → c20
#COMPARE(#0, #pos(z0)) → c5
MINSORT#1(nil) → c25
#CKLT(#LT) → c2
#COMPARE(#s(z0), #0) → c13
#COMPARE(#pos(z0), #neg(z1)) → c11
#COMPARE(#0, #s(z0)) → c6
#COMPARE(#pos(z0), #0) → c10
#COMPARE(#neg(z0), #0) → c7
#COMPARE(#0, #0) → c3
FINDMIN#1(nil) → c18
#CKLT(#GT) → c1
FINDMIN#3(#false, z0, z1, z2) → c21
#CKLT(#EQ) → c
#COMPARE(#0, #neg(z0)) → c4
#COMPARE(#neg(z0), #pos(z1)) → c9
FINDMIN#3(#true, z0, z1, z2) → c22

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
FINDMIN(z0) → c16(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN#2(::(z0, z1), z2) → c19(FINDMIN#3(#less(z2, z0), z2, z0, z1), #LESS(z2, z0))
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0))
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

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

Removed 2 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

FINDMIN(z0) → c16(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
#LESS(z0, z1) → c15(#COMPARE(z0, z1))
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

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

minSort(z0) → minSort#1(findMin(z0))
minSort#1(::(z0, z1)) → ::(z0, minSort(z1))
minSort#1(nil) → nil

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

findMin, findMin#1, findMin#2, findMin#3, #less, #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) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
We considered the (Usable) Rules:

findMin#2(nil, z0) → ::(z0, nil)
findMin#1(nil) → nil
findMin#3(#true, z0, z1, z2) → ::(z0, ::(z1, z2))
findMin#2(::(z0, z1), z2) → findMin#3(#less(z2, z0), z2, z0, z1)
findMin#3(#false, z0, z1, z2) → ::(z1, ::(z0, z2))
findMin(z0) → findMin#1(z0)
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0)
And the Tuples:

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

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

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
Defined Rule Symbols:

findMin, findMin#1, findMin#2, findMin#3, #less, #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

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

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

MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

findMin, findMin#1, findMin#2, findMin#3, #less, #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

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(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))
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
We considered the (Usable) Rules:

findMin#2(nil, z0) → ::(z0, nil)
#cklt(#GT) → #false
findMin#1(nil) → nil
findMin#3(#true, z0, z1, z2) → ::(z0, ::(z1, z2))
findMin#2(::(z0, z1), z2) → findMin#3(#less(z2, z0), z2, z0, z1)
findMin#3(#false, z0, z1, z2) → ::(z1, ::(z0, z2))
#cklt(#EQ) → #false
findMin(z0) → findMin#1(z0)
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0)
#less(z0, z1) → #cklt(#compare(z0, z1))
#cklt(#LT) → #true
And the Tuples:

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

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

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

FINDMIN(z0) → c16(FINDMIN#1(z0))
#LESS(z0, z1) → c15(#COMPARE(z0, z1))
K tuples:

MINSORT#1(::(z0, z1)) → c24(MINSORT(z1))
MINSORT(z0) → c23(MINSORT#1(findMin(z0)), FINDMIN(z0))
FINDMIN#1(::(z0, z1)) → c17(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN#2(::(z0, z1), z2) → c19(#LESS(z2, z0))
Defined Rule Symbols:

findMin, findMin#1, findMin#2, findMin#3, #less, #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

(15) CdtKnowledgeProof (EQUIVALENT transformation)

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

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

(16) BOUNDS(1, 1)