Runtime Complexity (innermost) proof of /tmp/tmpSRhAou/flatten.raml.xml

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

0 CpxRelTRS

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

↳2 CdtProblem

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

↳4 CdtProblem

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

↳6 CdtProblem

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

↳8 CdtProblem

↳9 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳10 CdtProblem

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

↳12 CdtProblem

↳13 CdtUsableRulesProof (⇔, 0 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 391 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 197 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 1269 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 940 ms)

↳22 CdtProblem

↳23 CdtKnowledgeProof (⇔, 0 ms)

↳24 BOUNDS(1, 1)

(0) Obligation:

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

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

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

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

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

#CKLT(#EQ) → c
#CKLT(#GT) → c1
#CKLT(#LT) → c2
#COMPARE(#0, #0) → c3
#COMPARE(#0, #neg(z0)) → c4
#COMPARE(#0, #pos(z0)) → c5
#COMPARE(#0, #s(z0)) → c6
#COMPARE(#neg(z0), #0) → c7
#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0))
#COMPARE(#neg(z0), #pos(z1)) → c9
#COMPARE(#pos(z0), #0) → c10
#COMPARE(#pos(z0), #neg(z1)) → c11
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #0) → c13
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1))
#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
APPEND#1(nil, z0) → c18
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(leaf) → c20
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTENSORT(z0) → c22(INSERTIONSORT(flatten(z0)), FLATTEN(z0))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#1(nil, z0) → c25
INSERT#2(#false, z0, z1, z2) → c26
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT#1(nil) → c30

S tuples:

#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
APPEND#1(nil, z0) → c18
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(leaf) → c20
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTENSORT(z0) → c22(INSERTIONSORT(flatten(z0)), FLATTEN(z0))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#1(nil, z0) → c25
INSERT#2(#false, z0, z1, z2) → c26
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT#1(nil) → c30

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:

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

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30

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

Removed 17 trailing nodes:

#CKLT(#LT) → c2
APPEND#1(nil, z0) → c18
#COMPARE(#s(z0), #0) → c13
INSERTIONSORT#1(nil) → c30
#COMPARE(#neg(z0), #0) → c7
#COMPARE(#pos(z0), #0) → c10
#CKLT(#EQ) → c
#COMPARE(#0, #neg(z0)) → c4
#COMPARE(#0, #pos(z0)) → c5
#COMPARE(#0, #0) → c3
INSERT#2(#false, z0, z1, z2) → c26
#COMPARE(#neg(z0), #pos(z1)) → c9
#COMPARE(#pos(z0), #neg(z1)) → c11
FLATTEN#1(leaf) → c20
INSERT#1(nil, z0) → c25
#COMPARE(#0, #s(z0)) → c6
#CKLT(#GT) → c1

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

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

S tuples:

#LESS(z0, z1) → c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTENSORT(z0) → c22(INSERTIONSORT(flatten(z0)), FLATTEN(z0))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
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

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

Removed 1 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

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

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTENSORT(z0) → c22(INSERTIONSORT(flatten(z0)), FLATTEN(z0))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#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

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

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

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

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#LESS(z0, z1) → c15(#COMPARE(z0, z1))
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))
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

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

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

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

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

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#LESS(z0, z1) → c15(#COMPARE(z0, z1))
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

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

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

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

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#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

(13) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

flattensort(z0) → insertionsort(flatten(z0))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
flatten(z0) → flatten#1(z0)
flatten#1(leaf) → nil
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2)))
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
#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)
insertionsort(z0) → insertionsort#1(z0)
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1))
insertionsort#1(nil) → nil
insert(z0, z1) → insert#1(z1, z0)
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1)
insert#1(nil, z0) → ::(z0, nil)
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2))
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2))

Tuples:

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

S tuples:

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

K tuples:

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

Defined Rule Symbols:

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

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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(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))
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:none
And the Tuples:

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

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

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

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
flatten(z0) → flatten#1(z0)
flatten#1(leaf) → nil
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2)))
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
#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)
insertionsort(z0) → insertionsort#1(z0)
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1))
insertionsort#1(nil) → nil
insert(z0, z1) → insert#1(z1, z0)
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1)
insert#1(nil, z0) → ::(z0, nil)
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2))
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2))

Tuples:

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

S tuples:

APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c(INSERTIONSORT(flatten(z0)))
FLATTEN(z0) → c19(FLATTEN#1(z0))
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:

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

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

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

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

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

We considered the (Usable) Rules:

flatten#1(leaf) → nil
flatten(z0) → flatten#1(z0)
append(z0, z1) → append#1(z0, z1)
append#1(nil, z0) → z0
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2)))
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))

And the Tuples:

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

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

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

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
flatten(z0) → flatten#1(z0)
flatten#1(leaf) → nil
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2)))
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
#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)
insertionsort(z0) → insertionsort#1(z0)
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1))
insertionsort#1(nil) → nil
insert(z0, z1) → insert#1(z1, z0)
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1)
insert#1(nil, z0) → ::(z0, nil)
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2))
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2))

Tuples:

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

S tuples:

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

K tuples:

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

Defined Rule Symbols:

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

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

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(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))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))

We considered the (Usable) Rules:

flatten#1(leaf) → nil
flatten(z0) → flatten#1(z0)
append(z0, z1) → append#1(z0, z1)
append#1(nil, z0) → z0
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2)))
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))

And the Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1))
APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#LESS(z0, z1) → c15(#COMPARE(z0, z1))
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(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) = 0
POL(#cklt(x₁)) = 0
POL(#compare(x₁, x₂)) = 0
POL(#false) = 0
POL(#less(x₁, x₂)) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = 0
POL(#true) = 0
POL(::(x₁, x₂)) = [1] + x₂
POL(APPEND(x₁, x₂)) = [1] + [2]x₁
POL(APPEND#1(x₁, x₂)) = [2]x₁
POL(FLATTEN(x₁)) = [2]x₁²
POL(FLATTEN#1(x₁)) = [2]x₁²
POL(FLATTENSORT(x₁)) = [2] + x₁ + x₁²
POL(INSERT(x₁, x₂)) = 0
POL(INSERT#1(x₁, x₂)) = 0
POL(INSERT#2(x₁, x₂, x₃, x₄)) = 0
POL(INSERTIONSORT(x₁)) = 0
POL(INSERTIONSORT#1(x₁)) = 0
POL(append(x₁, x₂)) = x₁ + x₂
POL(append#1(x₁, x₂)) = x₁ + x₂
POL(c(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c14(x₁)) = x₁
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c21(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c23(x₁)) = x₁
POL(c24(x₁, x₂)) = x₁ + x₂
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c29(x₁, x₂)) = x₁ + x₂
POL(c8(x₁)) = x₁
POL(flatten(x₁)) = [2]x₁
POL(flatten#1(x₁)) = [2]x₁
POL(insert(x₁, x₂)) = 0
POL(insert#1(x₁, x₂)) = 0
POL(insert#2(x₁, x₂, x₃, x₄)) = 0
POL(insertionsort(x₁)) = 0
POL(insertionsort#1(x₁)) = 0
POL(leaf) = 0
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
flatten(z0) → flatten#1(z0)
flatten#1(leaf) → nil
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2)))
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
#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)
insertionsort(z0) → insertionsort#1(z0)
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1))
insertionsort#1(nil) → nil
insert(z0, z1) → insert#1(z1, z0)
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1)
insert#1(nil, z0) → ::(z0, nil)
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2))
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2))

Tuples:

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

S tuples:

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

K tuples:

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

Defined Rule Symbols:

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

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

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

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

INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
#LESS(z0, z1) → c15(#COMPARE(z0, z1))

We considered the (Usable) Rules:

flatten#1(leaf) → nil
flatten(z0) → flatten#1(z0)
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2))
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1)
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2))
append(z0, z1) → append#1(z0, z1)
append#1(nil, z0) → z0
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2)))
insertionsort#1(nil) → nil
insert(z0, z1) → insert#1(z1, z0)
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1))
insert#1(nil, z0) → ::(z0, nil)
insertionsort(z0) → insertionsort#1(z0)
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))

And the Tuples:

#COMPARE(#neg(z0), #neg(z1)) → c8(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c12(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c14(#COMPARE(z0, z1))
APPEND(z0, z1) → c16(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c17(APPEND(z1, z2))
FLATTEN(z0) → c19(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c21(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERTIONSORT(z0) → c28(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c29(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#LESS(z0, z1) → c15(#COMPARE(z0, z1))
FLATTENSORT(z0) → c(INSERTIONSORT(flatten(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₂)) = [1]
POL(#LT) = 0
POL(#cklt(x₁)) = 0
POL(#compare(x₁, x₂)) = 0
POL(#false) = 0
POL(#less(x₁, x₂)) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = 0
POL(#true) = 0
POL(::(x₁, x₂)) = [1] + x₂
POL(APPEND(x₁, x₂)) = 0
POL(APPEND#1(x₁, x₂)) = 0
POL(FLATTEN(x₁)) = 0
POL(FLATTEN#1(x₁)) = 0
POL(FLATTENSORT(x₁)) = [2] + [3]x₁ + x₁²
POL(INSERT(x₁, x₂)) = [2]x₂
POL(INSERT#1(x₁, x₂)) = [2]x₁
POL(INSERT#2(x₁, x₂, x₃, x₄)) = [2]x₄
POL(INSERTIONSORT(x₁)) = [1] + x₁²
POL(INSERTIONSORT#1(x₁)) = [1] + x₁²
POL(append(x₁, x₂)) = x₁ + x₂
POL(append#1(x₁, x₂)) = x₁ + x₂
POL(c(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c14(x₁)) = x₁
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c21(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c23(x₁)) = x₁
POL(c24(x₁, x₂)) = x₁ + x₂
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c29(x₁, x₂)) = x₁ + x₂
POL(c8(x₁)) = x₁
POL(flatten(x₁)) = x₁
POL(flatten#1(x₁)) = x₁
POL(insert(x₁, x₂)) = [1] + x₂
POL(insert#1(x₁, x₂)) = [1] + x₁
POL(insert#2(x₁, x₂, x₃, x₄)) = [2] + x₄
POL(insertionsort(x₁)) = x₁
POL(insertionsort#1(x₁)) = x₁
POL(leaf) = 0
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = x₁ + x₂ + x₃

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1)
flatten(z0) → flatten#1(z0)
flatten#1(leaf) → nil
flatten#1(node(z0, z1, z2)) → append(z0, append(flatten(z1), flatten(z2)))
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
append#1(nil, z0) → z0
#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)
insertionsort(z0) → insertionsort#1(z0)
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1))
insertionsort#1(nil) → nil
insert(z0, z1) → insert#1(z1, z0)
insert#1(::(z0, z1), z2) → insert#2(#less(z0, z2), z2, z0, z1)
insert#1(nil, z0) → ::(z0, nil)
insert#2(#false, z0, z1, z2) → ::(z0, ::(z1, z2))
insert#2(#true, z0, z1, z2) → ::(z1, insert(z0, z2))

Tuples:

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

S tuples:

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

K tuples:

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

Defined Rule Symbols:

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

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

(23) CdtKnowledgeProof (EQUIVALENT transformation)

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

INSERT#2(#true, z0, z1, z2) → c27(INSERT(z0, z2))
INSERT(z0, z1) → c23(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c24(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))

Now S is empty

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(10) Obligation:

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

(12) Obligation:

(13) CdtUsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

(23) CdtKnowledgeProof (EQUIVALENT transformation)

(24) BOUNDS(1, 1)