22.34/6.12 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

22.34/6.12

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

0 CpxRelTRS

22.34/6.12

↳1 CpxRelTrsToCDT (UPPER BOUND (ID))

22.34/6.12

↳2 CdtProblem

22.34/6.12

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

22.34/6.12

↳4 CdtProblem

22.34/6.12

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

22.34/6.12

↳6 CdtProblem

22.34/6.12

↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)

22.34/6.12

↳8 CdtProblem

22.34/6.12

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

22.34/6.12

↳10 CdtProblem

22.34/6.12

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

22.34/6.12

↳12 CdtProblem

22.34/6.12

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

22.34/6.12

↳14 CdtProblem

22.34/6.12

↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

22.34/6.12

↳16 CdtProblem

22.34/6.12

↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

22.34/6.12

↳18 CdtProblem

22.34/6.12

↳19 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

22.34/6.12

↳20 CdtProblem

22.34/6.12

↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

22.34/6.12

↳22 CdtProblem

22.34/6.12

↳23 SIsEmptyProof (BOTH BOUNDS(ID, ID))

22.34/6.12

↳24 BOUNDS(O(1), O(1))

22.34/6.12

22.34/6.12 22.34/6.12

22.34/6.12

(0) Obligation:

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

#less(@x, @y) → #cklt(#compare(@x, @y)) 22.34/6.12
append(@l1, @l2) → append#1(@l1, @l2) 22.34/6.12
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) 22.34/6.12
append#1(nil, @l2) → @l2 22.34/6.12
flatten(@t) → flatten#1(@t) 22.34/6.12
flatten#1(leaf) → nil 22.34/6.12
flatten#1(node(@l, @t1, @t2)) → append(@l, append(flatten(@t1), flatten(@t2))) 22.34/6.12
flattensort(@t) → insertionsort(flatten(@t)) 22.34/6.12
insert(@x, @l) → insert#1(@l, @x) 22.34/6.12
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys) 22.34/6.12
insert#1(nil, @x) → ::(@x, nil) 22.34/6.12
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys)) 22.34/6.12
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys)) 22.34/6.12
insertionsort(@l) → insertionsort#1(@l) 22.34/6.12
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs)) 22.34/6.12
insertionsort#1(nil) → nil

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

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

Rewrite Strategy: INNERMOST

22.34/6.12

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

Relative innermost TRS to CDT Problem.

22.34/6.12

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.34/6.12
#cklt(#GT) → #false 22.34/6.12
#cklt(#LT) → #true 22.34/6.12
#compare(#0, #0) → #EQ 22.34/6.12
#compare(#0, #neg(z0)) → #GT 22.34/6.12
#compare(#0, #pos(z0)) → #LT 22.34/6.12
#compare(#0, #s(z0)) → #LT 22.34/6.12
#compare(#neg(z0), #0) → #LT 22.34/6.12
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.34/6.12
#compare(#neg(z0), #pos(z1)) → #LT 22.34/6.12
#compare(#pos(z0), #0) → #GT 22.34/6.12
#compare(#pos(z0), #neg(z1)) → #GT 22.34/6.12
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.34/6.12
#compare(#s(z0), #0) → #GT 22.34/6.12
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.34/6.12
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.34/6.12
append(z0, z1) → append#1(z0, z1) 22.34/6.12
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.34/6.12
append#1(nil, z0) → z0 22.34/6.12
flatten(z0) → flatten#1(z0) 22.34/6.12
flatten#1(leaf) → nil 22.34/6.12
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.34/6.12
flattensort(z0) → insertionsort(flatten(z0)) 22.34/6.12
insert(z0, z1) → insert#1(z1, z0) 22.34/6.12
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.34/6.12
insert#1(nil, z0) → ::(z0, nil) 22.34/6.12
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.34/6.12
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.34/6.12
insertionsort(z0) → insertionsort#1(z0) 22.34/6.12
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.34/6.12
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.34/6.12
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.34/6.12
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.34/6.12
#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) 22.34/6.12
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.34/6.12
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.34/6.12
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.34/6.12
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.34/6.12
FLATTENSORT(z0) → c22(INSERTIONSORT(flatten(z0)), FLATTEN(z0)) 22.34/6.12
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.34/6.12
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.34/6.12
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.34/6.12
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.34/6.12
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))

S tuples:

#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) 22.34/6.12
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.34/6.12
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.34/6.12
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.34/6.12
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.34/6.12
FLATTENSORT(z0) → c22(INSERTIONSORT(flatten(z0)), FLATTEN(z0)) 22.34/6.12
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.34/6.12
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.34/6.12
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.34/6.12
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.34/6.12
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))

K tuples:none
Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, #LESS, APPEND, APPEND#1, FLATTEN, FLATTEN#1, FLATTENSORT, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1

Compound Symbols:

c8, c12, c14, c15, c16, c17, c19, c21, c22, c23, c24, c27, c28, c29

22.34/6.12

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

Removed 1 trailing tuple parts

22.34/6.12

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.34/6.12
#cklt(#GT) → #false 22.34/6.12
#cklt(#LT) → #true 22.34/6.12
#compare(#0, #0) → #EQ 22.34/6.12
#compare(#0, #neg(z0)) → #GT 22.34/6.12
#compare(#0, #pos(z0)) → #LT 22.34/6.12
#compare(#0, #s(z0)) → #LT 22.34/6.12
#compare(#neg(z0), #0) → #LT 22.34/6.12
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.34/6.12
#compare(#neg(z0), #pos(z1)) → #LT 22.34/6.12
#compare(#pos(z0), #0) → #GT 22.34/6.12
#compare(#pos(z0), #neg(z1)) → #GT 22.34/6.12
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.34/6.12
#compare(#s(z0), #0) → #GT 22.34/6.12
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.34/6.12
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.34/6.12
append(z0, z1) → append#1(z0, z1) 22.34/6.12
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.34/6.12
append#1(nil, z0) → z0 22.34/6.12
flatten(z0) → flatten#1(z0) 22.34/6.12
flatten#1(leaf) → nil 22.34/6.12
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.34/6.12
flattensort(z0) → insertionsort(flatten(z0)) 22.34/6.12
insert(z0, z1) → insert#1(z1, z0) 22.34/6.12
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.34/6.12
insert#1(nil, z0) → ::(z0, nil) 22.34/6.12
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.34/6.12
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.34/6.12
insertionsort(z0) → insertionsort#1(z0) 22.34/6.12
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.34/6.12
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.34/6.12
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.34/6.12
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.34/6.12
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.34/6.12
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.34/6.12
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.34/6.12
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.34/6.12
FLATTENSORT(z0) → c22(INSERTIONSORT(flatten(z0)), FLATTEN(z0)) 22.34/6.12
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.34/6.12
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.34/6.12
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.34/6.12
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.34/6.12
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.34/6.12
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.34/6.12
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.34/6.12
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.34/6.12
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.34/6.12
FLATTENSORT(z0) → c22(INSERTIONSORT(flatten(z0)), FLATTEN(z0)) 22.34/6.12
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.34/6.12
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.34/6.12
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.34/6.12
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.34/6.12
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.34/6.12
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

K tuples:none
Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, FLATTENSORT, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c22, c23, c24, c27, c28, c29, c15

22.34/6.12

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

Split RHS of tuples not part of any SCC

22.34/6.12

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.34/6.12
#cklt(#GT) → #false 22.34/6.12
#cklt(#LT) → #true 22.34/6.12
#compare(#0, #0) → #EQ 22.34/6.12
#compare(#0, #neg(z0)) → #GT 22.34/6.12
#compare(#0, #pos(z0)) → #LT 22.34/6.12
#compare(#0, #s(z0)) → #LT 22.34/6.12
#compare(#neg(z0), #0) → #LT 22.34/6.12
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.34/6.12
#compare(#neg(z0), #pos(z1)) → #LT 22.34/6.12
#compare(#pos(z0), #0) → #GT 22.34/6.12
#compare(#pos(z0), #neg(z1)) → #GT 22.34/6.20
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.34/6.20
#compare(#s(z0), #0) → #GT 22.34/6.20
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.34/6.20
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.34/6.20
append(z0, z1) → append#1(z0, z1) 22.34/6.20
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.34/6.20
append#1(nil, z0) → z0 22.34/6.20
flatten(z0) → flatten#1(z0) 22.34/6.20
flatten#1(leaf) → nil 22.34/6.20
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.34/6.20
flattensort(z0) → insertionsort(flatten(z0)) 22.34/6.20
insert(z0, z1) → insert#1(z1, z0) 22.34/6.20
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.34/6.20
insert#1(nil, z0) → ::(z0, nil) 22.34/6.20
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.34/6.20
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.34/6.20
insertionsort(z0) → insertionsort#1(z0) 22.34/6.20
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.34/6.20
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.34/6.20
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.34/6.20
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.34/6.20
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.34/6.20
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.34/6.20
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.34/6.20
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.34/6.20
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.34/6.20
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.34/6.20
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.34/6.20
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.34/6.20
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.34/6.20
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.34/6.20
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0))) 22.34/6.20
FLATTENSORT(z0) → c(FLATTEN(z0))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.34/6.20
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.34/6.20
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.34/6.20
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.34/6.20
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.34/6.20
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.34/6.20
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.34/6.20
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.34/6.20
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.34/6.20
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.34/6.20
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0))) 22.34/6.20
FLATTENSORT(z0) → c(FLATTEN(z0))

K tuples:none
Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.34/6.20

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

FLATTENSORT(z0) → c(FLATTEN(z0))

22.34/6.20

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.34/6.20
#cklt(#GT) → #false 22.34/6.20
#cklt(#LT) → #true 22.34/6.20
#compare(#0, #0) → #EQ 22.34/6.20
#compare(#0, #neg(z0)) → #GT 22.34/6.20
#compare(#0, #pos(z0)) → #LT 22.34/6.20
#compare(#0, #s(z0)) → #LT 22.34/6.20
#compare(#neg(z0), #0) → #LT 22.34/6.20
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.34/6.20
#compare(#neg(z0), #pos(z1)) → #LT 22.34/6.20
#compare(#pos(z0), #0) → #GT 22.34/6.20
#compare(#pos(z0), #neg(z1)) → #GT 22.34/6.20
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.34/6.20
#compare(#s(z0), #0) → #GT 22.34/6.20
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.34/6.20
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.34/6.20
append(z0, z1) → append#1(z0, z1) 22.34/6.20
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.34/6.20
append#1(nil, z0) → z0 22.34/6.20
flatten(z0) → flatten#1(z0) 22.34/6.20
flatten#1(leaf) → nil 22.34/6.20
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.34/6.20
flattensort(z0) → insertionsort(flatten(z0)) 22.34/6.20
insert(z0, z1) → insert#1(z1, z0) 22.34/6.20
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.34/6.20
insert#1(nil, z0) → ::(z0, nil) 22.34/6.20
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.34/6.20
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.34/6.20
insertionsort(z0) → insertionsort#1(z0) 22.34/6.20
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.34/6.20
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.34/6.20
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.34/6.20
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.34/6.20
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.34/6.20
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.34/6.20
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.34/6.20
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.34/6.20
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.34/6.20
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.34/6.20
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.34/6.20
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.34/6.20
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.34/6.20
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.34/6.20
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.34/6.20
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.34/6.20
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.34/6.20
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.34/6.20
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.34/6.20
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.34/6.20
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.34/6.20
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.34/6.20
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.34/6.20
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.34/6.20
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

K tuples:none
Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.34/6.20

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

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

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

22.34/6.20

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.34/6.20
#cklt(#GT) → #false 22.34/6.20
#cklt(#LT) → #true 22.34/6.20
#compare(#0, #0) → #EQ 22.34/6.20
#compare(#0, #neg(z0)) → #GT 22.34/6.20
#compare(#0, #pos(z0)) → #LT 22.34/6.20
#compare(#0, #s(z0)) → #LT 22.34/6.20
#compare(#neg(z0), #0) → #LT 22.34/6.20
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.34/6.20
#compare(#neg(z0), #pos(z1)) → #LT 22.34/6.20
#compare(#pos(z0), #0) → #GT 22.34/6.20
#compare(#pos(z0), #neg(z1)) → #GT 22.34/6.20
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.34/6.20
#compare(#s(z0), #0) → #GT 22.34/6.20
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.34/6.20
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.34/6.20
append(z0, z1) → append#1(z0, z1) 22.34/6.20
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.34/6.20
append#1(nil, z0) → z0 22.34/6.20
flatten(z0) → flatten#1(z0) 22.34/6.20
flatten#1(leaf) → nil 22.34/6.20
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.34/6.20
flattensort(z0) → insertionsort(flatten(z0)) 22.34/6.20
insert(z0, z1) → insert#1(z1, z0) 22.34/6.20
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.34/6.20
insert#1(nil, z0) → ::(z0, nil) 22.34/6.20
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.34/6.20
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.34/6.20
insertionsort(z0) → insertionsort#1(z0) 22.34/6.20
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.34/6.20
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.34/6.20
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.69/6.21

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))

We considered the (Usable) Rules:

flatten(z0) → flatten#1(z0) 22.69/6.21
flatten#1(leaf) → nil 22.69/6.21
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.21
append(z0, z1) → append#1(z0, z1) 22.69/6.21
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.21
append#1(nil, z0) → z0 22.69/6.21
insertionsort(z0) → insertionsort#1(z0) 22.69/6.21
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.21
insertionsort#1(nil) → nil 22.69/6.21
insert(z0, z1) → insert#1(z1, z0) 22.69/6.21
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.21
insert#1(nil, z0) → ::(z0, nil) 22.69/6.21
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.21
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.21
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.21
#compare(#0, #0) → #EQ 22.69/6.21
#compare(#0, #neg(z0)) → #GT 22.69/6.21
#compare(#0, #pos(z0)) → #LT 22.69/6.21
#compare(#0, #s(z0)) → #LT 22.69/6.21
#compare(#neg(z0), #0) → #LT 22.69/6.21
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.21
#compare(#pos(z0), #0) → #GT 22.69/6.21
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.21
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.21
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#s(z0), #0) → #GT 22.69/6.21
#cklt(#EQ) → #false 22.69/6.21
#cklt(#GT) → #false 22.69/6.21
#cklt(#LT) → #true

And the Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.21
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

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

POL(#0) = 0 22.69/6.21
POL(#COMPARE(x₁, x₂)) = 0 22.69/6.21
POL(#EQ) = 0 22.69/6.21
POL(#GT) = 0 22.69/6.21
POL(#LESS(x₁, x₂)) = 0 22.69/6.21
POL(#LT) = 0 22.69/6.21
POL(#cklt(x₁)) = [3] 22.69/6.21
POL(#compare(x₁, x₂)) = [1] 22.69/6.21
POL(#false) = [1] 22.69/6.21
POL(#less(x₁, x₂)) = [1] 22.69/6.21
POL(#neg(x₁)) = 0 22.69/6.21
POL(#pos(x₁)) = 0 22.69/6.21
POL(#s(x₁)) = x₁ 22.69/6.21
POL(#true) = [4] 22.69/6.21
POL(::(x₁, x₂)) = [4] + x₂ 22.69/6.21
POL(APPEND(x₁, x₂)) = 0 22.69/6.21
POL(APPEND#1(x₁, x₂)) = 0 22.69/6.21
POL(FLATTEN(x₁)) = 0 22.69/6.21
POL(FLATTEN#1(x₁)) = 0 22.69/6.21
POL(FLATTENSORT(x₁)) = [5] + [3]x₁ 22.69/6.21
POL(INSERT(x₁, x₂)) = 0 22.69/6.21
POL(INSERT#1(x₁, x₂)) = 0 22.69/6.21
POL(INSERT#2(x₁, x₂, x₃, x₄)) = 0 22.69/6.21
POL(INSERTIONSORT(x₁)) = [2]x₁ 22.69/6.21
POL(INSERTIONSORT#1(x₁)) = [2]x₁ 22.69/6.21
POL(append(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(append#1(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(c(x₁)) = x₁ 22.69/6.21
POL(c12(x₁)) = x₁ 22.69/6.21
POL(c14(x₁)) = x₁ 22.69/6.21
POL(c15(x₁)) = x₁ 22.69/6.21
POL(c16(x₁)) = x₁ 22.69/6.21
POL(c17(x₁)) = x₁ 22.69/6.21
POL(c19(x₁)) = x₁ 22.69/6.21
POL(c21(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄ 22.69/6.21
POL(c23(x₁)) = x₁ 22.69/6.21
POL(c24(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(c27(x₁)) = x₁ 22.69/6.21
POL(c28(x₁)) = x₁ 22.69/6.21
POL(c29(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(c8(x₁)) = x₁ 22.69/6.21
POL(flatten(x₁)) = x₁ 22.69/6.21
POL(flatten#1(x₁)) = x₁ 22.69/6.21
POL(insert(x₁, x₂)) = [4] + x₂ 22.69/6.21
POL(insert#1(x₁, x₂)) = [4] + x₁ 22.69/6.21
POL(insert#2(x₁, x₂, x₃, x₄)) = [4] + [4]x₁ + x₄ 22.69/6.21
POL(insertionsort(x₁)) = x₁ 22.69/6.21
POL(insertionsort#1(x₁)) = x₁ 22.69/6.21
POL(leaf) = 0 22.69/6.21
POL(nil) = 0 22.69/6.21
POL(node(x₁, x₂, x₃)) = x₁ + x₂ + x₃

22.69/6.21

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.69/6.21
#cklt(#GT) → #false 22.69/6.21
#cklt(#LT) → #true 22.69/6.21
#compare(#0, #0) → #EQ 22.69/6.21
#compare(#0, #neg(z0)) → #GT 22.69/6.21
#compare(#0, #pos(z0)) → #LT 22.69/6.21
#compare(#0, #s(z0)) → #LT 22.69/6.21
#compare(#neg(z0), #0) → #LT 22.69/6.21
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.21
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.21
#compare(#pos(z0), #0) → #GT 22.69/6.21
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.21
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#s(z0), #0) → #GT 22.69/6.21
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.21
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.21
append(z0, z1) → append#1(z0, z1) 22.69/6.21
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.21
append#1(nil, z0) → z0 22.69/6.21
flatten(z0) → flatten#1(z0) 22.69/6.21
flatten#1(leaf) → nil 22.69/6.21
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.21
flattensort(z0) → insertionsort(flatten(z0)) 22.69/6.21
insert(z0, z1) → insert#1(z1, z0) 22.69/6.21
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.21
insert#1(nil, z0) → ::(z0, nil) 22.69/6.21
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.21
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.21
insertionsort(z0) → insertionsort#1(z0) 22.69/6.21
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.21
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.21
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0))) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))

Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.69/6.21

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

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

INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))

22.69/6.21

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.69/6.21
#cklt(#GT) → #false 22.69/6.21
#cklt(#LT) → #true 22.69/6.21
#compare(#0, #0) → #EQ 22.69/6.21
#compare(#0, #neg(z0)) → #GT 22.69/6.21
#compare(#0, #pos(z0)) → #LT 22.69/6.21
#compare(#0, #s(z0)) → #LT 22.69/6.21
#compare(#neg(z0), #0) → #LT 22.69/6.21
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.21
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.21
#compare(#pos(z0), #0) → #GT 22.69/6.21
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.21
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#s(z0), #0) → #GT 22.69/6.21
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.21
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.21
append(z0, z1) → append#1(z0, z1) 22.69/6.21
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.21
append#1(nil, z0) → z0 22.69/6.21
flatten(z0) → flatten#1(z0) 22.69/6.21
flatten#1(leaf) → nil 22.69/6.21
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.21
flattensort(z0) → insertionsort(flatten(z0)) 22.69/6.21
insert(z0, z1) → insert#1(z1, z0) 22.69/6.21
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.21
insert#1(nil, z0) → ::(z0, nil) 22.69/6.21
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.21
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.21
insertionsort(z0) → insertionsort#1(z0) 22.69/6.21
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.21
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.21
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0))) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))

Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.69/6.21

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

FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))

We considered the (Usable) Rules:

flatten(z0) → flatten#1(z0) 22.69/6.21
flatten#1(leaf) → nil 22.69/6.21
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.21
append(z0, z1) → append#1(z0, z1) 22.69/6.21
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.21
append#1(nil, z0) → z0 22.69/6.21
insertionsort(z0) → insertionsort#1(z0) 22.69/6.21
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.21
insertionsort#1(nil) → nil 22.69/6.21
insert(z0, z1) → insert#1(z1, z0) 22.69/6.21
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.21
insert#1(nil, z0) → ::(z0, nil) 22.69/6.21
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.21
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.21
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.21
#compare(#0, #0) → #EQ 22.69/6.21
#compare(#0, #neg(z0)) → #GT 22.69/6.21
#compare(#0, #pos(z0)) → #LT 22.69/6.21
#compare(#0, #s(z0)) → #LT 22.69/6.21
#compare(#neg(z0), #0) → #LT 22.69/6.21
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.21
#compare(#pos(z0), #0) → #GT 22.69/6.21
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.21
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.21
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#s(z0), #0) → #GT 22.69/6.21
#cklt(#EQ) → #false 22.69/6.21
#cklt(#GT) → #false 22.69/6.21
#cklt(#LT) → #true

And the Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.21
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

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

POL(#0) = 0 22.69/6.21
POL(#COMPARE(x₁, x₂)) = 0 22.69/6.21
POL(#EQ) = [2] 22.69/6.21
POL(#GT) = [4] 22.69/6.21
POL(#LESS(x₁, x₂)) = 0 22.69/6.21
POL(#LT) = 0 22.69/6.21
POL(#cklt(x₁)) = [4]x₁ 22.69/6.21
POL(#compare(x₁, x₂)) = 0 22.69/6.21
POL(#false) = [4] 22.69/6.21
POL(#less(x₁, x₂)) = 0 22.69/6.21
POL(#neg(x₁)) = 0 22.69/6.21
POL(#pos(x₁)) = x₁ 22.69/6.21
POL(#s(x₁)) = x₁ 22.69/6.21
POL(#true) = 0 22.69/6.21
POL(::(x₁, x₂)) = 0 22.69/6.21
POL(APPEND(x₁, x₂)) = 0 22.69/6.21
POL(APPEND#1(x₁, x₂)) = 0 22.69/6.21
POL(FLATTEN(x₁)) = [1] + [4]x₁ 22.69/6.21
POL(FLATTEN#1(x₁)) = [4]x₁ 22.69/6.21
POL(FLATTENSORT(x₁)) = [3] + [5]x₁ 22.69/6.21
POL(INSERT(x₁, x₂)) = 0 22.69/6.21
POL(INSERT#1(x₁, x₂)) = 0 22.69/6.21
POL(INSERT#2(x₁, x₂, x₃, x₄)) = 0 22.69/6.21
POL(INSERTIONSORT(x₁)) = 0 22.69/6.21
POL(INSERTIONSORT#1(x₁)) = 0 22.69/6.21
POL(append(x₁, x₂)) = 0 22.69/6.21
POL(append#1(x₁, x₂)) = [3] + [3]x₂ 22.69/6.21
POL(c(x₁)) = x₁ 22.69/6.21
POL(c12(x₁)) = x₁ 22.69/6.21
POL(c14(x₁)) = x₁ 22.69/6.21
POL(c15(x₁)) = x₁ 22.69/6.21
POL(c16(x₁)) = x₁ 22.69/6.21
POL(c17(x₁)) = x₁ 22.69/6.21
POL(c19(x₁)) = x₁ 22.69/6.21
POL(c21(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄ 22.69/6.21
POL(c23(x₁)) = x₁ 22.69/6.21
POL(c24(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(c27(x₁)) = x₁ 22.69/6.21
POL(c28(x₁)) = x₁ 22.69/6.21
POL(c29(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(c8(x₁)) = x₁ 22.69/6.21
POL(flatten(x₁)) = 0 22.69/6.21
POL(flatten#1(x₁)) = [3] + [3]x₁ 22.69/6.21
POL(insert(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ 22.69/6.21
POL(insert#1(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ 22.69/6.21
POL(insert#2(x₁, x₂, x₃, x₄)) = [3] + [3]x₂ + [3]x₃ + [3]x₄ 22.69/6.21
POL(insertionsort(x₁)) = 0 22.69/6.21
POL(insertionsort#1(x₁)) = [3] + [3]x₁ 22.69/6.21
POL(leaf) = [1] 22.69/6.21
POL(nil) = 0 22.69/6.21
POL(node(x₁, x₂, x₃)) = [4] + x₂ + x₃

22.69/6.21

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.69/6.21
#cklt(#GT) → #false 22.69/6.21
#cklt(#LT) → #true 22.69/6.21
#compare(#0, #0) → #EQ 22.69/6.21
#compare(#0, #neg(z0)) → #GT 22.69/6.21
#compare(#0, #pos(z0)) → #LT 22.69/6.21
#compare(#0, #s(z0)) → #LT 22.69/6.21
#compare(#neg(z0), #0) → #LT 22.69/6.21
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.21
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.21
#compare(#pos(z0), #0) → #GT 22.69/6.21
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.21
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#s(z0), #0) → #GT 22.69/6.21
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.21
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.21
append(z0, z1) → append#1(z0, z1) 22.69/6.21
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.21
append#1(nil, z0) → z0 22.69/6.21
flatten(z0) → flatten#1(z0) 22.69/6.21
flatten#1(leaf) → nil 22.69/6.21
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.21
flattensort(z0) → insertionsort(flatten(z0)) 22.69/6.21
insert(z0, z1) → insert#1(z1, z0) 22.69/6.21
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.21
insert#1(nil, z0) → ::(z0, nil) 22.69/6.21
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.21
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.21
insertionsort(z0) → insertionsort#1(z0) 22.69/6.21
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.21
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.21
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0))) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))

Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.69/6.21

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

INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))

We considered the (Usable) Rules:

flatten(z0) → flatten#1(z0) 22.69/6.21
flatten#1(leaf) → nil 22.69/6.21
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.21
append(z0, z1) → append#1(z0, z1) 22.69/6.21
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.21
append#1(nil, z0) → z0 22.69/6.21
insertionsort(z0) → insertionsort#1(z0) 22.69/6.21
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.21
insertionsort#1(nil) → nil 22.69/6.21
insert(z0, z1) → insert#1(z1, z0) 22.69/6.21
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.21
insert#1(nil, z0) → ::(z0, nil) 22.69/6.21
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.21
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.21
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.21
#compare(#0, #0) → #EQ 22.69/6.21
#compare(#0, #neg(z0)) → #GT 22.69/6.21
#compare(#0, #pos(z0)) → #LT 22.69/6.21
#compare(#0, #s(z0)) → #LT 22.69/6.21
#compare(#neg(z0), #0) → #LT 22.69/6.21
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.21
#compare(#pos(z0), #0) → #GT 22.69/6.21
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.21
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.21
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#s(z0), #0) → #GT 22.69/6.21
#cklt(#EQ) → #false 22.69/6.21
#cklt(#GT) → #false 22.69/6.21
#cklt(#LT) → #true

And the Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.21
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

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

POL(#0) = [2] 22.69/6.21
POL(#COMPARE(x₁, x₂)) = 0 22.69/6.21
POL(#EQ) = 0 22.69/6.21
POL(#GT) = 0 22.69/6.21
POL(#LESS(x₁, x₂)) = 0 22.69/6.21
POL(#LT) = [1] 22.69/6.21
POL(#cklt(x₁)) = x₁ 22.69/6.21
POL(#compare(x₁, x₂)) = [2]x₁·x₂ 22.69/6.21
POL(#false) = 0 22.69/6.21
POL(#less(x₁, x₂)) = [2]x₁·x₂ 22.69/6.21
POL(#neg(x₁)) = [2] + x₁ 22.69/6.21
POL(#pos(x₁)) = [2] + x₁ 22.69/6.21
POL(#s(x₁)) = [2] + x₁ 22.69/6.21
POL(#true) = [1] 22.69/6.21
POL(::(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(APPEND(x₁, x₂)) = 0 22.69/6.21
POL(APPEND#1(x₁, x₂)) = 0 22.69/6.21
POL(FLATTEN(x₁)) = 0 22.69/6.21
POL(FLATTEN#1(x₁)) = 0 22.69/6.21
POL(FLATTENSORT(x₁)) = [1] + x₁² 22.69/6.21
POL(INSERT(x₁, x₂)) = [2]x₁·x₂ 22.69/6.21
POL(INSERT#1(x₁, x₂)) = [2]x₁·x₂ 22.69/6.21
POL(INSERT#2(x₁, x₂, x₃, x₄)) = x₁ + [2]x₂·x₄ 22.69/6.21
POL(INSERTIONSORT(x₁)) = x₁² 22.69/6.21
POL(INSERTIONSORT#1(x₁)) = x₁² 22.69/6.21
POL(append(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(append#1(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(c(x₁)) = x₁ 22.69/6.21
POL(c12(x₁)) = x₁ 22.69/6.21
POL(c14(x₁)) = x₁ 22.69/6.21
POL(c15(x₁)) = x₁ 22.69/6.21
POL(c16(x₁)) = x₁ 22.69/6.21
POL(c17(x₁)) = x₁ 22.69/6.21
POL(c19(x₁)) = x₁ 22.69/6.21
POL(c21(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄ 22.69/6.21
POL(c23(x₁)) = x₁ 22.69/6.21
POL(c24(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(c27(x₁)) = x₁ 22.69/6.21
POL(c28(x₁)) = x₁ 22.69/6.21
POL(c29(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(c8(x₁)) = x₁ 22.69/6.21
POL(flatten(x₁)) = x₁ 22.69/6.21
POL(flatten#1(x₁)) = x₁ 22.69/6.21
POL(insert(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(insert#1(x₁, x₂)) = x₁ + x₂ 22.69/6.21
POL(insert#2(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄ 22.69/6.21
POL(insertionsort(x₁)) = x₁ 22.69/6.21
POL(insertionsort#1(x₁)) = x₁ 22.69/6.21
POL(leaf) = 0 22.69/6.21
POL(nil) = 0 22.69/6.21
POL(node(x₁, x₂, x₃)) = x₁ + x₂ + x₃

22.69/6.21

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.69/6.21
#cklt(#GT) → #false 22.69/6.21
#cklt(#LT) → #true 22.69/6.21
#compare(#0, #0) → #EQ 22.69/6.21
#compare(#0, #neg(z0)) → #GT 22.69/6.21
#compare(#0, #pos(z0)) → #LT 22.69/6.21
#compare(#0, #s(z0)) → #LT 22.69/6.21
#compare(#neg(z0), #0) → #LT 22.69/6.21
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.21
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.21
#compare(#pos(z0), #0) → #GT 22.69/6.21
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.21
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#s(z0), #0) → #GT 22.69/6.21
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.21
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.21
append(z0, z1) → append#1(z0, z1) 22.69/6.21
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.21
append#1(nil, z0) → z0 22.69/6.21
flatten(z0) → flatten#1(z0) 22.69/6.21
flatten#1(leaf) → nil 22.69/6.21
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.21
flattensort(z0) → insertionsort(flatten(z0)) 22.69/6.21
insert(z0, z1) → insert#1(z1, z0) 22.69/6.21
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.21
insert#1(nil, z0) → ::(z0, nil) 22.69/6.21
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.21
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.21
insertionsort(z0) → insertionsort#1(z0) 22.69/6.21
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.21
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.21
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0))) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))

Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.69/6.21

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

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

INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

22.69/6.21

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.69/6.21
#cklt(#GT) → #false 22.69/6.21
#cklt(#LT) → #true 22.69/6.21
#compare(#0, #0) → #EQ 22.69/6.21
#compare(#0, #neg(z0)) → #GT 22.69/6.21
#compare(#0, #pos(z0)) → #LT 22.69/6.21
#compare(#0, #s(z0)) → #LT 22.69/6.21
#compare(#neg(z0), #0) → #LT 22.69/6.21
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.21
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.21
#compare(#pos(z0), #0) → #GT 22.69/6.21
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.21
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.21
#compare(#s(z0), #0) → #GT 22.69/6.21
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.21
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.21
append(z0, z1) → append#1(z0, z1) 22.69/6.21
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.21
append#1(nil, z0) → z0 22.69/6.21
flatten(z0) → flatten#1(z0) 22.69/6.21
flatten#1(leaf) → nil 22.69/6.21
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.21
flattensort(z0) → insertionsort(flatten(z0)) 22.69/6.21
insert(z0, z1) → insert#1(z1, z0) 22.69/6.21
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.21
insert#1(nil, z0) → ::(z0, nil) 22.69/6.21
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.21
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.21
insertionsort(z0) → insertionsort#1(z0) 22.69/6.21
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.21
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.21
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.21
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.21
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.21
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))

K tuples:

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0))) 22.69/6.21
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.21
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.21
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.21
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.21
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.21
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.21
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.21
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.69/6.21

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

APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.21
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))

We considered the (Usable) Rules:

flatten(z0) → flatten#1(z0) 22.69/6.22
flatten#1(leaf) → nil 22.69/6.22
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.22
append(z0, z1) → append#1(z0, z1) 22.69/6.22
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.22
append#1(nil, z0) → z0 22.69/6.22
insertionsort(z0) → insertionsort#1(z0) 22.69/6.22
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.22
insertionsort#1(nil) → nil 22.69/6.22
insert(z0, z1) → insert#1(z1, z0) 22.69/6.22
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.22
insert#1(nil, z0) → ::(z0, nil) 22.69/6.22
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.22
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.22
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.22
#compare(#0, #0) → #EQ 22.69/6.22
#compare(#0, #neg(z0)) → #GT 22.69/6.22
#compare(#0, #pos(z0)) → #LT 22.69/6.22
#compare(#0, #s(z0)) → #LT 22.69/6.22
#compare(#neg(z0), #0) → #LT 22.69/6.22
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.22
#compare(#pos(z0), #0) → #GT 22.69/6.22
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.22
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.22
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.22
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.22
#compare(#s(z0), #0) → #GT 22.69/6.22
#cklt(#EQ) → #false 22.69/6.22
#cklt(#GT) → #false 22.69/6.22
#cklt(#LT) → #true

And the Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.22
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.22
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.22
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.22
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.22
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.22
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.22
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.22
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.22
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.22
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.22
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.22
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.22
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

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

POL(#0) = [3] 22.69/6.22
POL(#COMPARE(x₁, x₂)) = 0 22.69/6.22
POL(#EQ) = 0 22.69/6.22
POL(#GT) = [1] 22.69/6.22
POL(#LESS(x₁, x₂)) = 0 22.69/6.22
POL(#LT) = 0 22.69/6.22
POL(#cklt(x₁)) = [2]x₁ 22.69/6.22
POL(#compare(x₁, x₂)) = 0 22.69/6.22
POL(#false) = 0 22.69/6.22
POL(#less(x₁, x₂)) = 0 22.69/6.22
POL(#neg(x₁)) = 0 22.69/6.22
POL(#pos(x₁)) = 0 22.69/6.22
POL(#s(x₁)) = 0 22.69/6.22
POL(#true) = 0 22.69/6.22
POL(::(x₁, x₂)) = [2] + x₂ 22.69/6.22
POL(APPEND(x₁, x₂)) = [2] + [2]x₁ 22.69/6.22
POL(APPEND#1(x₁, x₂)) = [2]x₁ 22.69/6.22
POL(FLATTEN(x₁)) = [2] + x₁² 22.69/6.22
POL(FLATTEN#1(x₁)) = x₁² 22.69/6.22
POL(FLATTENSORT(x₁)) = [1] + x₁² 22.69/6.22
POL(INSERT(x₁, x₂)) = 0 22.69/6.22
POL(INSERT#1(x₁, x₂)) = 0 22.69/6.22
POL(INSERT#2(x₁, x₂, x₃, x₄)) = 0 22.69/6.22
POL(INSERTIONSORT(x₁)) = 0 22.69/6.22
POL(INSERTIONSORT#1(x₁)) = 0 22.69/6.22
POL(append(x₁, x₂)) = x₁ + x₂ 22.69/6.22
POL(append#1(x₁, x₂)) = x₁ + x₂ 22.69/6.22
POL(c(x₁)) = x₁ 22.69/6.22
POL(c12(x₁)) = x₁ 22.69/6.22
POL(c14(x₁)) = x₁ 22.69/6.22
POL(c15(x₁)) = x₁ 22.69/6.22
POL(c16(x₁)) = x₁ 22.69/6.22
POL(c17(x₁)) = x₁ 22.69/6.22
POL(c19(x₁)) = x₁ 22.69/6.22
POL(c21(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄ 22.69/6.22
POL(c23(x₁)) = x₁ 22.69/6.22
POL(c24(x₁, x₂)) = x₁ + x₂ 22.69/6.22
POL(c27(x₁)) = x₁ 22.69/6.22
POL(c28(x₁)) = x₁ 22.69/6.22
POL(c29(x₁, x₂)) = x₁ + x₂ 22.69/6.22
POL(c8(x₁)) = x₁ 22.69/6.22
POL(flatten(x₁)) = [2]x₁ 22.69/6.22
POL(flatten#1(x₁)) = [2]x₁ 22.69/6.22
POL(insert(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ + [3]x₂² + [3]x₁·x₂ + [3]x₁² 22.69/6.22
POL(insert#1(x₁, x₂)) = [3] + [3]x₂ + [3]x₂² 22.69/6.22
POL(insert#2(x₁, x₂, x₃, x₄)) = [3] + [3]x₂ + [3]x₃ + [3]x₄ + [3]x₄² + [3]x₃·x₄ + [3]x₂·x₄ + [3]x₃² + [3]x₂·x₃ + [3]x₂² 22.69/6.22
POL(insertionsort(x₁)) = 0 22.69/6.22
POL(insertionsort#1(x₁)) = [3] 22.69/6.22
POL(leaf) = 0 22.69/6.22
POL(nil) = 0 22.69/6.22
POL(node(x₁, x₂, x₃)) = [3] + x₁ + x₂ + x₃

22.69/6.22

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

#cklt(#EQ) → #false 22.69/6.22
#cklt(#GT) → #false 22.69/6.22
#cklt(#LT) → #true 22.69/6.22
#compare(#0, #0) → #EQ 22.69/6.22
#compare(#0, #neg(z0)) → #GT 22.69/6.22
#compare(#0, #pos(z0)) → #LT 22.69/6.22
#compare(#0, #s(z0)) → #LT 22.69/6.22
#compare(#neg(z0), #0) → #LT 22.69/6.22
#compare(#neg(z0), #neg(z1)) → #compare(z1, z0) 22.69/6.22
#compare(#neg(z0), #pos(z1)) → #LT 22.69/6.22
#compare(#pos(z0), #0) → #GT 22.69/6.22
#compare(#pos(z0), #neg(z1)) → #GT 22.69/6.22
#compare(#pos(z0), #pos(z1)) → #compare(z0, z1) 22.69/6.22
#compare(#s(z0), #0) → #GT 22.69/6.22
#compare(#s(z0), #s(z1)) → #compare(z0, z1) 22.69/6.22
#less(z0, z1) → #cklt(#compare(z0, z1)) 22.69/6.22
append(z0, z1) → append#1(z0, z1) 22.69/6.22
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 22.69/6.22
append#1(nil, z0) → z0 22.69/6.22
flatten(z0) → flatten#1(z0) 22.69/6.22
flatten#1(leaf) → nil 22.69/6.22
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2))) 22.69/6.22
flattensort(z0) → insertionsort(flatten(z0)) 22.69/6.22
insert(z0, z1) → insert#1(z1, z0) 22.69/6.22
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1) 22.69/6.22
insert#1(nil, z0) → ::(z0, nil) 22.69/6.22
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2)) 22.69/6.22
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2)) 22.69/6.22
insertionsort(z0) → insertionsort#1(z0) 22.69/6.22
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1)) 22.69/6.22
insertionsort#1(nil) → nil

Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0)) 22.69/6.22
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1)) 22.69/6.22
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1)) 22.69/6.22
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.22
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2)) 22.69/6.22
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.22
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.22
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.22
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.22
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.22
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.22
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.22
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.22
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))

S tuples:none
K tuples:

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0))) 22.69/6.22
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1)) 22.69/6.22
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0)) 22.69/6.22
FLATTEN(z0) → c19(FLATTEN#1(z0)) 22.69/6.22
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2)) 22.69/6.22
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2)) 22.69/6.22
INSERT(z0, z1) → c23(INSERT#1(z1, z0)) 22.69/6.22
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2)) 22.69/6.22
#LESS(z0, z1) → c15(#COMPARE(z0, z1)) 22.69/6.22
APPEND(z0, z1) → c16(APPEND#1(z0, z1)) 22.69/6.22
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))

Defined Rule Symbols:

#less, append, append#1, flatten, flatten#1, flattensort, insert, insert#1, insert#2, insertionsort, insertionsort#1, #cklt, #compare

Defined Pair Symbols:

#COMPARE, APPEND, APPEND#1, FLATTEN, FLATTEN#1, INSERT, INSERT#1, INSERT#2, INSERTIONSORT, INSERTIONSORT#1, #LESS, FLATTENSORT

Compound Symbols:

c8, c12, c14, c16, c17, c19, c21, c23, c24, c27, c28, c29, c15, c

22.69/6.22

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

The set S is empty

22.69/6.22

(24) BOUNDS(O(1), O(1))

22.69/6.22