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

(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) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

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

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

Infered types.

(4) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#compare, append, append#1, flatten, flatten#1, insertionsort, insert, insert#1, insertionsort#1

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1
insertionsort = insertionsort#1
insert = insert#1
insert < insertionsort#1

(6) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
#compare, append, append#1, flatten, flatten#1, insertionsort, insert, insert#1, insertionsort#1

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1
insertionsort = insertionsort#1
insert = insert#1
insert < insertionsort#1

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)

Induction Base:
#compare(gen_#0:#neg:#pos:#s6_3(0), gen_#0:#neg:#pos:#s6_3(0)) →_R^Ω(0)
#EQ

Induction Step:
#compare(gen_#0:#neg:#pos:#s6_3(+(n10_3, 1)), gen_#0:#neg:#pos:#s6_3(+(n10_3, 1))) →_R^Ω(0)
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) →_IH
#EQ

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n⁰).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
insert#1, append, append#1, flatten, flatten#1, insertionsort, insert, insertionsort#1

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1
insertionsort = insertionsort#1
insert = insert#1
insert < insertionsort#1

(10) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insert#1.

(11) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
insert, append, append#1, flatten, flatten#1, insertionsort, insertionsort#1

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1
insertionsort = insertionsort#1
insert = insert#1
insert < insertionsort#1

(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insert.

(13) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
insertionsort#1, append, append#1, flatten, flatten#1, insertionsort

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1
insertionsort = insertionsort#1

(14) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsort#1(gen_:::nil7_3(n319403_3)) → *9_3, rt ∈ Ω(n319403₃)

Induction Base:
insertionsort#1(gen_:::nil7_3(0))

Induction Step:
insertionsort#1(gen_:::nil7_3(+(n319403_3, 1))) →_R^Ω(1)
insert(#0, insertionsort(gen_:::nil7_3(n319403_3))) →_R^Ω(1)
insert(#0, insertionsort#1(gen_:::nil7_3(n319403_3))) →_IH
insert(#0, *9_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(15) Complex Obligation (BEST)

(16) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n319403_3)) → *9_3, rt ∈ Ω(n319403₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
insertionsort, append, append#1, flatten, flatten#1

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1
insertionsort = insertionsort#1

(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)

Induction Base:
insertionsort(gen_:::nil7_3(0))

Induction Step:
insertionsort(gen_:::nil7_3(+(n322738_3, 1))) →_R^Ω(1)
insertionsort#1(gen_:::nil7_3(+(n322738_3, 1))) →_R^Ω(1)
insert(#0, insertionsort(gen_:::nil7_3(n322738_3))) →_IH
insert(#0, *9_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(18) Complex Obligation (BEST)

(19) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n319403_3)) → *9_3, rt ∈ Ω(n319403₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
insertionsort#1, append, append#1, flatten, flatten#1

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1
insertionsort = insertionsort#1

(20) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)

Induction Base:
insertionsort#1(gen_:::nil7_3(0))

Induction Step:
insertionsort#1(gen_:::nil7_3(+(n331473_3, 1))) →_R^Ω(1)
insert(#0, insertionsort(gen_:::nil7_3(n331473_3))) →_R^Ω(1)
insert(#0, insertionsort#1(gen_:::nil7_3(n331473_3))) →_IH
insert(#0, *9_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(21) Complex Obligation (BEST)

(22) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
append#1, append, flatten, flatten#1

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1

(23) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
append#1(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b)) → gen_:::nil7_3(+(n345620_3, b)), rt ∈ Ω(1 + n345620₃)

Induction Base:
append#1(gen_:::nil7_3(0), gen_:::nil7_3(b)) →_R^Ω(1)
gen_:::nil7_3(b)

Induction Step:
append#1(gen_:::nil7_3(+(n345620_3, 1)), gen_:::nil7_3(b)) →_R^Ω(1)
::(#0, append(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b))) →_R^Ω(1)
::(#0, append#1(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b))) →_IH
::(#0, gen_:::nil7_3(+(b, c345621_3)))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(24) Complex Obligation (BEST)

(25) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)
append#1(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b)) → gen_:::nil7_3(+(n345620_3, b)), rt ∈ Ω(1 + n345620₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
append, flatten, flatten#1

They will be analysed ascendingly in the following order:
append = append#1
append < flatten#1
flatten = flatten#1

(26) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol append.

(27) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)
append#1(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b)) → gen_:::nil7_3(+(n345620_3, b)), rt ∈ Ω(1 + n345620₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
flatten#1, flatten

They will be analysed ascendingly in the following order:
flatten = flatten#1

(28) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
flatten#1(gen_leaf:node8_3(n347247_3)) → gen_:::nil7_3(0), rt ∈ Ω(1 + n347247₃)

Induction Base:
flatten#1(gen_leaf:node8_3(0)) →_R^Ω(1)
nil

Induction Step:
flatten#1(gen_leaf:node8_3(+(n347247_3, 1))) →_R^Ω(1)
append(nil, append(flatten(leaf), flatten(gen_leaf:node8_3(n347247_3)))) →_R^Ω(1)
append(nil, append(flatten#1(leaf), flatten(gen_leaf:node8_3(n347247_3)))) →_R^Ω(1)
append(nil, append(nil, flatten(gen_leaf:node8_3(n347247_3)))) →_R^Ω(1)
append(nil, append(nil, flatten#1(gen_leaf:node8_3(n347247_3)))) →_IH
append(nil, append(nil, gen_:::nil7_3(0))) →_R^Ω(1)
append(nil, append#1(nil, gen_:::nil7_3(0))) →_L^Ω(1)
append(nil, gen_:::nil7_3(+(0, 0))) →_R^Ω(1)
append#1(nil, gen_:::nil7_3(0)) →_L^Ω(1)
gen_:::nil7_3(+(0, 0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(29) Complex Obligation (BEST)

(30) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)
append#1(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b)) → gen_:::nil7_3(+(n345620_3, b)), rt ∈ Ω(1 + n345620₃)
flatten#1(gen_leaf:node8_3(n347247_3)) → gen_:::nil7_3(0), rt ∈ Ω(1 + n347247₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

The following defined symbols remain to be analysed:
flatten

They will be analysed ascendingly in the following order:
flatten = flatten#1

(31) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol flatten.

(32) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)
append#1(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b)) → gen_:::nil7_3(+(n345620_3, b)), rt ∈ Ω(1 + n345620₃)
flatten#1(gen_leaf:node8_3(n347247_3)) → gen_:::nil7_3(0), rt ∈ Ω(1 + n347247₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)

(34) BOUNDS(n^1, INF)

(35) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)
append#1(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b)) → gen_:::nil7_3(+(n345620_3, b)), rt ∈ Ω(1 + n345620₃)
flatten#1(gen_leaf:node8_3(n347247_3)) → gen_:::nil7_3(0), rt ∈ Ω(1 + n347247₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

No more defined symbols left to analyse.

(36) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)

(37) BOUNDS(n^1, INF)

(38) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)
append#1(gen_:::nil7_3(n345620_3), gen_:::nil7_3(b)) → gen_:::nil7_3(+(n345620_3, b)), rt ∈ Ω(1 + n345620₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

No more defined symbols left to analyse.

(39) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)

(40) BOUNDS(n^1, INF)

(41) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

No more defined symbols left to analyse.

(42) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsort#1(gen_:::nil7_3(n331473_3)) → *9_3, rt ∈ Ω(n331473₃)

(43) BOUNDS(n^1, INF)

(44) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n319403_3)) → *9_3, rt ∈ Ω(n319403₃)
insertionsort(gen_:::nil7_3(n322738_3)) → *9_3, rt ∈ Ω(n322738₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

No more defined symbols left to analyse.

(45) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsort#1(gen_:::nil7_3(n319403_3)) → *9_3, rt ∈ Ω(n319403₃)

(46) BOUNDS(n^1, INF)

(47) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)
insertionsort#1(gen_:::nil7_3(n319403_3)) → *9_3, rt ∈ Ω(n319403₃)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

No more defined symbols left to analyse.

(48) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsort#1(gen_:::nil7_3(n319403_3)) → *9_3, rt ∈ Ω(n319403₃)

(49) BOUNDS(n^1, INF)

(50) Obligation:

Innermost TRS:
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)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_#0:#neg:#pos:#s2_3 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
hole_leaf:node5_3 :: leaf:node
gen_#0:#neg:#pos:#s6_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil7_3 :: Nat → :::nil
gen_leaf:node8_3 :: Nat → leaf:node

Lemmas:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s6_3(0) ⇔ #0
gen_#0:#neg:#pos:#s6_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s6_3(x))
gen_:::nil7_3(0) ⇔ nil
gen_:::nil7_3(+(x, 1)) ⇔ ::(#0, gen_:::nil7_3(x))
gen_leaf:node8_3(0) ⇔ leaf
gen_leaf:node8_3(+(x, 1)) ⇔ node(nil, leaf, gen_leaf:node8_3(x))

No more defined symbols left to analyse.

(51) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#compare(gen_#0:#neg:#pos:#s6_3(n10_3), gen_#0:#neg:#pos:#s6_3(n10_3)) → #EQ, rt ∈ Ω(0)

(52) BOUNDS(1, INF)