Runtime Complexity (innermost) proof of /tmp/tmpEZ

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

0 CpxRelTRS

↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)

↳2 CpxTRS

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

↳4 CdtProblem

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

↳6 CdtProblem

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

↳8 CdtProblem

↳9 CdtUsableRulesProof (⇔, 0 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 238 ms)

↳12 CdtProblem

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

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 494 ms)

↳16 CdtProblem

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

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)), 1555 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)), 1380 ms)

↳22 CdtProblem

↳23 CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)), 996 ms)

↳24 CdtProblem

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

↳26 BOUNDS(1, 1)

(0) Obligation:

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

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) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

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

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
#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

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

#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
#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:

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

S tuples:

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

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

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

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

Removed 17 trailing nodes:

#COMPARE(#pos(z0), #0) → c21
#CKLT(#GT) → c12
#COMPARE(#neg(z0), #pos(z1)) → c20
#CKLT(#LT) → c13
FINDMIN#3(#true, z0, z1, z2) → c7
#CKLT(#EQ) → c11
FINDMIN#3(#false, z0, z1, z2) → c6
FINDMIN#1(nil) → c3
#COMPARE(#0, #neg(z0)) → c15
#COMPARE(#0, #0) → c14
#COMPARE(#pos(z0), #neg(z1)) → c22
MINSORT#1(nil) → c10
FINDMIN#2(nil, z0) → c5
#COMPARE(#0, #s(z0)) → c17
#COMPARE(#s(z0), #0) → c24
#COMPARE(#0, #pos(z0)) → c16
#COMPARE(#neg(z0), #0) → c18

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

#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
#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:

#LESS(z0, z1) → c(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN#2(::(z0, z1), z2) → c4(FINDMIN#3(#less(z2, z0), z2, z0, z1), #LESS(z2, z0))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))

S tuples:

#LESS(z0, z1) → c(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN#2(::(z0, z1), z2) → c4(FINDMIN#3(#less(z2, z0), z2, z0, z1), #LESS(z2, z0))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c1, c2, c4, c8, c9, c19, c23, c25

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

Removed 2 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

#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
#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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#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:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

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

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

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

(11) 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(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))

We considered the (Usable) Rules:

findMin#2(nil, z0) → ::(z0, nil)
#compare(#0, #neg(z0)) → #GT
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))
#compare(#0, #pos(z0)) → #LT
findMin(z0) → findMin#1(z0)
#compare(#0, #s(z0)) → #LT
#compare(#pos(z0), #0) → #GT
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0)
#cklt(#GT) → #false
#compare(#s(z0), #s(z1)) → #compare(z0, z1)
#compare(#0, #0) → #EQ
#compare(#s(z0), #0) → #GT
#compare(#neg(z0), #pos(z1)) → #LT
#compare(#neg(z0), #0) → #LT
#cklt(#EQ) → #false
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1)
#compare(#pos(z0), #neg(z1)) → #GT
findMin#1(::(z0, z1)) → findMin#2(findMin(z1), z0)
#less(z0, z1) → #cklt(#compare(z0, z1))
#cklt(#LT) → #true

And the Tuples:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

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

POL(#0) = 0
POL(#COMPARE(x₁, x₂)) = 0
POL(#EQ) = [1]
POL(#GT) = [1]
POL(#LESS(x₁, x₂)) = 0
POL(#LT) = [1]
POL(#cklt(x₁)) = x₁
POL(#compare(x₁, x₂)) = [1]
POL(#false) = [1]
POL(#less(x₁, x₂)) = [1]
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = 0
POL(#true) = [1]
POL(::(x₁, x₂)) = [1] + x₂
POL(FINDMIN(x₁)) = 0
POL(FINDMIN#1(x₁)) = 0
POL(FINDMIN#2(x₁, x₂)) = 0
POL(MINSORT(x₁)) = [1] + x₁
POL(MINSORT#1(x₁)) = x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(findMin(x₁)) = x₁
POL(findMin#1(x₁)) = x₁
POL(findMin#2(x₁, x₂)) = [1] + x₁
POL(findMin#3(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₄
POL(nil) = [1]

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

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

K tuples:

MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

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

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

MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))

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

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

K tuples:

MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

(15) 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)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

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

POL(#0) = 0
POL(#COMPARE(x₁, x₂)) = 0
POL(#EQ) = 0
POL(#GT) = 0
POL(#LESS(x₁, x₂)) = 0
POL(#LT) = [2]
POL(#cklt(x₁)) = [1]
POL(#compare(x₁, x₂)) = 0
POL(#false) = 0
POL(#less(x₁, x₂)) = x₁ + [2]x₁²
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = [1]
POL(#true) = 0
POL(::(x₁, x₂)) = [1] + x₂
POL(FINDMIN(x₁)) = [2]x₁
POL(FINDMIN#1(x₁)) = [2]x₁
POL(FINDMIN#2(x₁, x₂)) = 0
POL(MINSORT(x₁)) = [1] + [2]x₁ + [2]x₁²
POL(MINSORT#1(x₁)) = [2]x₁²
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(findMin(x₁)) = x₁
POL(findMin#1(x₁)) = x₁
POL(findMin#2(x₁, x₂)) = [1] + x₁
POL(findMin#3(x₁, x₂, x₃, x₄)) = [2] + x₄
POL(nil) = 0

(16) 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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:

FINDMIN(z0) → c1(FINDMIN#1(z0))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

K tuples:

MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

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

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

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

(18) 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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:

#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))

K tuples:

MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

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

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

#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))

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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

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

POL(#0) = 0
POL(#COMPARE(x₁, x₂)) = x₁·x₂
POL(#EQ) = 0
POL(#GT) = 0
POL(#LESS(x₁, x₂)) = x₁ + x₁·x₂
POL(#LT) = 0
POL(#cklt(x₁)) = [1]
POL(#compare(x₁, x₂)) = 0
POL(#false) = [1]
POL(#less(x₁, x₂)) = [1]
POL(#neg(x₁)) = x₁
POL(#pos(x₁)) = x₁
POL(#s(x₁)) = [1] + x₁
POL(#true) = [1]
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(FINDMIN(x₁)) = x₁²
POL(FINDMIN#1(x₁)) = x₁²
POL(FINDMIN#2(x₁, x₂)) = x₂ + x₁·x₂
POL(MINSORT(x₁)) = x₁ + x₁² + x₁³
POL(MINSORT#1(x₁)) = x₁³
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(findMin(x₁)) = x₁
POL(findMin#1(x₁)) = x₁
POL(findMin#2(x₁, x₂)) = [1] + x₁ + x₂
POL(findMin#3(x₁, x₂, x₃, x₄)) = [1] + x₂ + x₃ + x₄ + x₁³
POL(nil) = 0

(20) 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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:

#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))

K tuples:

MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

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

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

#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, 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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

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

POL(#0) = 0
POL(#COMPARE(x₁, x₂)) = x₁·x₂
POL(#EQ) = 0
POL(#GT) = 0
POL(#LESS(x₁, x₂)) = x₁·x₂
POL(#LT) = 0
POL(#cklt(x₁)) = [1]
POL(#compare(x₁, x₂)) = 0
POL(#false) = [1]
POL(#less(x₁, x₂)) = [1]
POL(#neg(x₁)) = [1] + x₁
POL(#pos(x₁)) = x₁
POL(#s(x₁)) = x₁
POL(#true) = [1]
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(FINDMIN(x₁)) = x₁²
POL(FINDMIN#1(x₁)) = x₁²
POL(FINDMIN#2(x₁, x₂)) = [1] + x₁·x₂
POL(MINSORT(x₁)) = x₁² + x₁³
POL(MINSORT#1(x₁)) = x₁³
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(findMin(x₁)) = x₁
POL(findMin#1(x₁)) = x₁
POL(findMin#2(x₁, x₂)) = [1] + x₁ + x₂
POL(findMin#3(x₁, x₂, x₃, x₄)) = [1] + x₂ + x₃ + x₄ + x₁²
POL(nil) = 0

(22) 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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:

#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))

K tuples:

MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

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

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

#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))

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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

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

POL(#0) = 0
POL(#COMPARE(x₁, x₂)) = x₁·x₂
POL(#EQ) = 0
POL(#GT) = 0
POL(#LESS(x₁, x₂)) = x₁ + x₁·x₂
POL(#LT) = 0
POL(#cklt(x₁)) = [1]
POL(#compare(x₁, x₂)) = 0
POL(#false) = [1]
POL(#less(x₁, x₂)) = [1]
POL(#neg(x₁)) = x₁
POL(#pos(x₁)) = [1] + x₁
POL(#s(x₁)) = [1] + x₁
POL(#true) = [1]
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(FINDMIN(x₁)) = x₁²
POL(FINDMIN#1(x₁)) = x₁²
POL(FINDMIN#2(x₁, x₂)) = x₁·x₂
POL(MINSORT(x₁)) = [1] + x₁ + x₁² + x₁³
POL(MINSORT#1(x₁)) = x₁³
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(findMin(x₁)) = x₁
POL(findMin#1(x₁)) = x₁
POL(findMin#2(x₁, x₂)) = [1] + x₁ + x₂
POL(findMin#3(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₂ + x₃ + x₄
POL(nil) = 0

(24) 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:

FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))

S tuples:none
K tuples:

MINSORT(z0) → c8(MINSORT#1(findMin(z0)), FINDMIN(z0))
MINSORT#1(::(z0, z1)) → c9(MINSORT(z1))
FINDMIN#1(::(z0, z1)) → c2(FINDMIN#2(findMin(z1), z0), FINDMIN(z1))
FINDMIN(z0) → c1(FINDMIN#1(z0))
FINDMIN#2(::(z0, z1), z2) → c4(#LESS(z2, z0))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c25(#COMPARE(z0, z1))
#COMPARE(#neg(z0), #neg(z1)) → c19(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c23(#COMPARE(z0, z1))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c8, c9, c19, c23, c25, c, c4

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

The set S is empty

(0) Obligation:

(1) RelTrsToTrsProof (UPPER BOUND(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) CdtUsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) BOUNDS(1, 1)