Runtime Complexity (innermost) proof of /tmp/tmpOD_4W

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

0 CpxRelTRS

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

↳2 CpxTRS

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

↳4 CdtProblem

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

↳6 CdtProblem

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

↳8 CdtProblem

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

↳10 CdtProblem

↳11 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳12 CdtProblem

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

↳14 CdtProblem

↳15 CdtUsableRulesProof (⇔, 0 ms)

↳16 CdtProblem

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

↳18 CdtProblem

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

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 198 ms)

↳22 CdtProblem

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

↳24 CdtProblem

↳25 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 1038 ms)

↳26 CdtProblem

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

↳28 CdtProblem

↳29 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 679 ms)

↳30 CdtProblem

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

↳32 CdtProblem

↳33 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 613 ms)

↳34 CdtProblem

↳35 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 591 ms)

↳36 CdtProblem

↳37 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 486 ms)

↳38 CdtProblem

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

↳40 BOUNDS(1, 1)

(0) Obligation:

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

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

transformed relative TRS to TRS

(2) Obligation:

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

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
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

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

S tuples:

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

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

Compound Symbols:

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

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

Removed 17 trailing nodes:

INSERT#1(nil, z0) → c10
FLATTEN#1(leaf) → c5
#COMPARE(#0, #neg(z0)) → c20
INSERTIONSORT#1(nil) → c15
#CKLT(#LT) → c18
#COMPARE(#pos(z0), #0) → c26
#CKLT(#GT) → c17
#COMPARE(#0, #0) → c19
#COMPARE(#neg(z0), #pos(z1)) → c25
#COMPARE(#neg(z0), #0) → c23
#CKLT(#EQ) → c16
#COMPARE(#0, #s(z0)) → c22
INSERT#2(#false, z0, z1, z2) → c11
#COMPARE(#pos(z0), #neg(z1)) → c27
APPEND#1(nil, z0) → c3
#COMPARE(#0, #pos(z0)) → c21
#COMPARE(#s(z0), #0) → c29

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

#LESS(z0, z1) → c(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTENSORT(z0) → c7(INSERTIONSORT(flatten(z0)), FLATTEN(z0))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))

S tuples:

#LESS(z0, z1) → c(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTENSORT(z0) → c7(INSERTIONSORT(flatten(z0)), FLATTEN(z0))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#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:

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

Compound Symbols:

c, c1, c2, c4, c6, c7, c8, c9, c12, c13, c14, c24, c28, c30

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

Removed 1 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTENSORT(z0) → c7(INSERTIONSORT(flatten(z0)), FLATTEN(z0))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTENSORT(z0) → c7(INSERTIONSORT(flatten(z0)), FLATTEN(z0))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#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:

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

Compound Symbols:

c1, c2, c4, c6, c7, c8, c9, c12, c13, c14, c24, c28, c30, c

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

Split RHS of tuples not part of any SCC

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
FLATTENSORT(z0) → c3(FLATTEN(z0))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
FLATTENSORT(z0) → c3(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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

FLATTENSORT(z0) → c3(FLATTEN(z0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

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

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

(15) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

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

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

(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#1(::(z0, z1)) → c14(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:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(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₂)) = 0
POL(APPEND#1(x₁, x₂)) = 0
POL(FLATTEN(x₁)) = 0
POL(FLATTEN#1(x₁)) = 0
POL(FLATTENSORT(x₁)) = x₁
POL(INSERT(x₁, x₂)) = 0
POL(INSERT#1(x₁, x₂)) = 0
POL(INSERT#2(x₁, x₂, x₃, x₄)) = 0
POL(INSERTIONSORT(x₁)) = x₁
POL(INSERTIONSORT#1(x₁)) = x₁
POL(append(x₁, x₂)) = x₁ + x₂
POL(append#1(x₁, x₂)) = x₁ + x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂
POL(flatten(x₁)) = x₁
POL(flatten#1(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(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:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

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

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

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

(21) 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#1(node(z0, z1, z2)) → c6(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:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(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) = [1]
POL(#GT) = 0
POL(#LESS(x₁, x₂)) = 0
POL(#LT) = [1]
POL(#cklt(x₁)) = x₁
POL(#compare(x₁, x₂)) = 0
POL(#false) = 0
POL(#less(x₁, x₂)) = [1]
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = 0
POL(#true) = 0
POL(::(x₁, x₂)) = 0
POL(APPEND(x₁, x₂)) = 0
POL(APPEND#1(x₁, x₂)) = 0
POL(FLATTEN(x₁)) = x₁
POL(FLATTEN#1(x₁)) = x₁
POL(FLATTENSORT(x₁)) = [1]
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₂)) = 0
POL(append#1(x₁, x₂)) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂
POL(flatten(x₁)) = 0
POL(flatten#1(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(leaf) = 0
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = [1] + 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:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

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

FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

(25) 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) → c1(APPEND#1(z0, 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:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(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) = [2]
POL(#GT) = [1]
POL(#LESS(x₁, x₂)) = 0
POL(#LT) = 0
POL(#cklt(x₁)) = 0
POL(#compare(x₁, x₂)) = 0
POL(#false) = [2]
POL(#less(x₁, x₂)) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = [1]
POL(#true) = 0
POL(::(x₁, x₂)) = [2] + x₂
POL(APPEND(x₁, x₂)) = [2] + x₁
POL(APPEND#1(x₁, x₂)) = x₁
POL(FLATTEN(x₁)) = x₁²
POL(FLATTEN#1(x₁)) = x₁²
POL(FLATTENSORT(x₁)) = [2] + [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₁)) = [2]x₁
POL(INSERTIONSORT#1(x₁)) = [2]x₁
POL(append(x₁, x₂)) = x₁ + x₂
POL(append#1(x₁, x₂)) = x₁ + x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂
POL(flatten(x₁)) = x₁
POL(flatten#1(x₁)) = x₁
POL(insert(x₁, x₂)) = [2] + [2]x₂ + [2]x₁²
POL(insert#1(x₁, x₂)) = [1] + x₁ + [2]x₂ + [2]x₁²
POL(insert#2(x₁, x₂, x₃, x₄)) = [1] + x₄² + [2]x₃·x₄ + [2]x₂·x₄ + x₁·x₄ + [2]x₁² + [2]x₁·x₂ + [2]x₁·x₃ + [2]x₃² + [2]x₂²
POL(insertionsort(x₁)) = 0
POL(insertionsort#1(x₁)) = [1]
POL(leaf) = [1]
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
APPEND(z0, z1) → c1(APPEND#1(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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

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

APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

(29) 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#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#LESS(z0, z1) → c(#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))
#cklt(#GT) → #false
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)
#cklt(#EQ) → #false
insertionsort#1(::(z0, z1)) → insert(z0, insertionsort(z1))
insert#1(nil, z0) → ::(z0, nil)
insertionsort(z0) → insertionsort#1(z0)
#less(z0, z1) → #cklt(#compare(z0, z1))
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
#cklt(#LT) → #true

And the Tuples:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

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

POL(#0) = [1]
POL(#COMPARE(x₁, x₂)) = 0
POL(#EQ) = 0
POL(#GT) = 0
POL(#LESS(x₁, x₂)) = [2]
POL(#LT) = 0
POL(#cklt(x₁)) = [2]
POL(#compare(x₁, x₂)) = 0
POL(#false) = [2]
POL(#less(x₁, x₂)) = [2]
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = [2]
POL(#true) = [2]
POL(::(x₁, x₂)) = [2] + 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] + [2]x₁ + x₁²
POL(INSERT(x₁, x₂)) = [2]x₂
POL(INSERT#1(x₁, x₂)) = [2]x₁
POL(INSERT#2(x₁, x₂, x₃, x₄)) = [2] + [2]x₄
POL(INSERTIONSORT(x₁)) = x₁²
POL(INSERTIONSORT#1(x₁)) = x₁²
POL(append(x₁, x₂)) = x₁ + x₂
POL(append#1(x₁, x₂)) = x₁ + x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂
POL(flatten(x₁)) = x₁
POL(flatten#1(x₁)) = x₁
POL(insert(x₁, x₂)) = [2] + x₂
POL(insert#1(x₁, x₂)) = [2] + x₁
POL(insert#2(x₁, x₂, x₃, x₄)) = x₄ + x₁²
POL(insertionsort(x₁)) = [2]x₁
POL(insertionsort#1(x₁)) = [2]x₁
POL(leaf) = 0
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = x₁ + x₂ + x₃

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#LESS(z0, z1) → c(#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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

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

INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#LESS(z0, z1) → c(#COMPARE(z0, z1))

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

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

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

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

POL(#0) = 0
POL(#COMPARE(x₁, x₂)) = x₁·x₂
POL(#EQ) = 0
POL(#GT) = [1]
POL(#LESS(x₁, x₂)) = x₁·x₂
POL(#LT) = 0
POL(#cklt(x₁)) = [2]
POL(#compare(x₁, x₂)) = 0
POL(#false) = 0
POL(#less(x₁, x₂)) = 0
POL(#neg(x₁)) = x₁
POL(#pos(x₁)) = [2] + x₁
POL(#s(x₁)) = x₁
POL(#true) = 0
POL(::(x₁, x₂)) = x₁ + 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] + [2]x₁ + [2]x₁²
POL(INSERT(x₁, x₂)) = [2]x₁·x₂
POL(INSERT#1(x₁, x₂)) = [2]x₁·x₂
POL(INSERT#2(x₁, x₂, x₃, x₄)) = [2]x₂·x₄
POL(INSERTIONSORT(x₁)) = [2]x₁²
POL(INSERTIONSORT#1(x₁)) = [2]x₁²
POL(append(x₁, x₂)) = x₁ + x₂
POL(append#1(x₁, x₂)) = x₁ + x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂
POL(flatten(x₁)) = x₁
POL(flatten#1(x₁)) = x₁
POL(insert(x₁, x₂)) = x₁ + x₂
POL(insert#1(x₁, x₂)) = x₁ + x₂
POL(insert#2(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(insertionsort(x₁)) = x₁
POL(insertionsort#1(x₁)) = x₁
POL(leaf) = [2]
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = x₁ + x₂ + x₃

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
#COMPARE(#pos(z0), #pos(z1)) → c28(#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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

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

#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))

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:

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

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

POL(#0) = 0
POL(#COMPARE(x₁, x₂)) = [2]x₁·x₂
POL(#EQ) = [2]
POL(#GT) = 0
POL(#LESS(x₁, x₂)) = [2]x₁·x₂
POL(#LT) = 0
POL(#cklt(x₁)) = [1]
POL(#compare(x₁, x₂)) = 0
POL(#false) = 0
POL(#less(x₁, x₂)) = [2]x₁ + x₁²
POL(#neg(x₁)) = [2] + x₁
POL(#pos(x₁)) = [1] + x₁
POL(#s(x₁)) = x₁
POL(#true) = [2]
POL(::(x₁, x₂)) = x₁ + 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]x₁ + [2]x₁²
POL(INSERT(x₁, x₂)) = [2]x₁·x₂
POL(INSERT#1(x₁, x₂)) = [2]x₁·x₂
POL(INSERT#2(x₁, x₂, x₃, x₄)) = [2]x₂·x₄
POL(INSERTIONSORT(x₁)) = x₁²
POL(INSERTIONSORT#1(x₁)) = x₁²
POL(append(x₁, x₂)) = x₁ + x₂
POL(append#1(x₁, x₂)) = x₁ + x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂
POL(flatten(x₁)) = x₁
POL(flatten#1(x₁)) = x₁
POL(insert(x₁, x₂)) = x₁ + x₂
POL(insert#1(x₁, x₂)) = x₁ + x₂
POL(insert#2(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(insertionsort(x₁)) = x₁
POL(insertionsort#1(x₁)) = x₁
POL(leaf) = 0
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = x₁ + x₂ + x₃

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:

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

K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))

Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

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

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

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

POL(#0) = [1]
POL(#COMPARE(x₁, x₂)) = [2]x₁·x₂
POL(#EQ) = [1]
POL(#GT) = 0
POL(#LESS(x₁, x₂)) = [2]x₁·x₂
POL(#LT) = 0
POL(#cklt(x₁)) = [1]
POL(#compare(x₁, x₂)) = x₂ + [2]x₂² + [2]x₁·x₂
POL(#false) = 0
POL(#less(x₁, x₂)) = x₁·x₂
POL(#neg(x₁)) = x₁
POL(#pos(x₁)) = x₁
POL(#s(x₁)) = [1] + x₁
POL(#true) = [1]
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(APPEND(x₁, x₂)) = 0
POL(APPEND#1(x₁, x₂)) = 0
POL(FLATTEN(x₁)) = 0
POL(FLATTEN#1(x₁)) = 0
POL(FLATTENSORT(x₁)) = x₁ + [2]x₁²
POL(INSERT(x₁, x₂)) = [2]x₁·x₂
POL(INSERT#1(x₁, x₂)) = [2]x₁·x₂
POL(INSERT#2(x₁, x₂, x₃, x₄)) = [2]x₂·x₄
POL(INSERTIONSORT(x₁)) = x₁²
POL(INSERTIONSORT#1(x₁)) = x₁²
POL(append(x₁, x₂)) = x₁ + x₂
POL(append#1(x₁, x₂)) = x₁ + x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c6(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂
POL(flatten(x₁)) = x₁
POL(flatten#1(x₁)) = x₁
POL(insert(x₁, x₂)) = [1] + x₁ + x₂
POL(insert#1(x₁, x₂)) = [1] + x₁ + x₂
POL(insert#2(x₁, x₂, x₃, x₄)) = [2] + x₂ + x₃ + x₄
POL(insertionsort(x₁)) = x₁
POL(insertionsort#1(x₁)) = x₁
POL(leaf) = 0
POL(nil) = 0
POL(node(x₁, x₂, x₃)) = x₁ + x₂ + x₃

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

APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#s(z0), #s(z1)) → c30(#COMPARE(z0, z1))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))

S tuples:none
K tuples:

FLATTENSORT(z0) → c3(INSERTIONSORT(flatten(z0)))
INSERTIONSORT#1(::(z0, z1)) → c14(INSERT(z0, insertionsort(z1)), INSERTIONSORT(z1))
INSERTIONSORT(z0) → c13(INSERTIONSORT#1(z0))
FLATTEN#1(node(z0, z1, z2)) → c6(APPEND(z0, append(flatten(z1), flatten(z2))), APPEND(flatten(z1), flatten(z2)), FLATTEN(z1), FLATTEN(z2))
FLATTEN(z0) → c4(FLATTEN#1(z0))
APPEND(z0, z1) → c1(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c2(APPEND(z1, z2))
INSERT#2(#true, z0, z1, z2) → c12(INSERT(z0, z2))
#LESS(z0, z1) → c(#COMPARE(z0, z1))
INSERT(z0, z1) → c8(INSERT#1(z1, z0))
INSERT#1(::(z0, z1), z2) → c9(INSERT#2(#less(z0, z2), z2, z0, z1), #LESS(z0, z2))
#COMPARE(#pos(z0), #pos(z1)) → c28(#COMPARE(z0, z1))
#COMPARE(#neg(z0), #neg(z1)) → c24(#COMPARE(z1, z0))
#COMPARE(#s(z0), #s(z1)) → c30(#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:

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

Compound Symbols:

c1, c2, c4, c6, c8, c9, c12, c13, c14, c24, c28, c30, c, c3

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

The set S is empty

(0) Obligation:

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(12) Obligation:

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

(14) Obligation:

(15) CdtUsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) BOUNDS(1, 1)