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

merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


merge'(nil', y) → y
merge'(x, nil') → x
merge'(.'(x, y), .'(u, v)) → if'(<'(x, u), .'(x, merge'(y, .'(u, v))), .'(u, merge'(.'(x, y), v)))
++'(nil', y) → y
++'(.'(x, y), z) → .'(x, ++'(y, z))
if'(true', x, y) → x
if'(false', x, y) → x

Rewrite Strategy: INNERMOST

Sliced the following arguments:
.'/0
<'/0
<'/1

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


merge'(nil', y) → y
merge'(x, nil') → x
merge'(.'(y), .'(v)) → if'(<', .'(merge'(y, .'(v))), .'(merge'(.'(y), v)))
++'(nil', y) → y
++'(.'(y), z) → .'(++'(y, z))
if'(true', x, y) → x
if'(false', x, y) → x

Rewrite Strategy: INNERMOST

Infered types.

Rules:
merge'(nil', y) → y
merge'(x, nil') → x
merge'(.'(y), .'(v)) → if'(<', .'(merge'(y, .'(v))), .'(merge'(.'(y), v)))
++'(nil', y) → y
++'(.'(y), z) → .'(++'(y, z))
if'(true', x, y) → x
if'(false', x, y) → x

Types:
merge' :: nil':.' → nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.'
if' :: <':true':false' → nil':.' → nil':.' → nil':.'
<' :: <':true':false'
++' :: nil':.' → nil':.' → nil':.'
true' :: <':true':false'
false' :: <':true':false'
_hole_nil':.'1 :: nil':.'
_hole_<':true':false'2 :: <':true':false'
_gen_nil':.'3 :: Nat → nil':.'

Heuristically decided to analyse the following defined symbols:
merge', ++'

Rules:
merge'(nil', y) → y
merge'(x, nil') → x
merge'(.'(y), .'(v)) → if'(<', .'(merge'(y, .'(v))), .'(merge'(.'(y), v)))
++'(nil', y) → y
++'(.'(y), z) → .'(++'(y, z))
if'(true', x, y) → x
if'(false', x, y) → x

Types:
merge' :: nil':.' → nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.'
if' :: <':true':false' → nil':.' → nil':.' → nil':.'
<' :: <':true':false'
++' :: nil':.' → nil':.' → nil':.'
true' :: <':true':false'
false' :: <':true':false'
_hole_nil':.'1 :: nil':.'
_hole_<':true':false'2 :: <':true':false'
_gen_nil':.'3 :: Nat → nil':.'

Generator Equations:
_gen_nil':.'3(0) ⇔ nil'
_gen_nil':.'3(+(x, 1)) ⇔ .'(_gen_nil':.'3(x))

The following defined symbols remain to be analysed:
merge', ++'

Proved the following rewrite lemma:
merge'(_gen_nil':.'3(+(1, _n5)), _gen_nil':.'3(1)) → _*4, rt ∈ Ω(n5)

Induction Base:
merge'(_gen_nil':.'3(+(1, 0)), _gen_nil':.'3(1))

Induction Step:
merge'(_gen_nil':.'3(+(1, +(_$n6, 1))), _gen_nil':.'3(1)) →RΩ(1)
if'(<', .'(merge'(_gen_nil':.'3(+(1, _$n6)), .'(_gen_nil':.'3(0)))), .'(merge'(.'(_gen_nil':.'3(+(1, _$n6))), _gen_nil':.'3(0)))) →IH
if'(<', .'(_*4), .'(merge'(.'(_gen_nil':.'3(+(1, _$n6))), _gen_nil':.'3(0)))) →RΩ(1)
if'(<', .'(_*4), .'(.'(_gen_nil':.'3(+(1, _$n6)))))

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

Rules:
merge'(nil', y) → y
merge'(x, nil') → x
merge'(.'(y), .'(v)) → if'(<', .'(merge'(y, .'(v))), .'(merge'(.'(y), v)))
++'(nil', y) → y
++'(.'(y), z) → .'(++'(y, z))
if'(true', x, y) → x
if'(false', x, y) → x

Types:
merge' :: nil':.' → nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.'
if' :: <':true':false' → nil':.' → nil':.' → nil':.'
<' :: <':true':false'
++' :: nil':.' → nil':.' → nil':.'
true' :: <':true':false'
false' :: <':true':false'
_hole_nil':.'1 :: nil':.'
_hole_<':true':false'2 :: <':true':false'
_gen_nil':.'3 :: Nat → nil':.'

Lemmas:
merge'(_gen_nil':.'3(+(1, _n5)), _gen_nil':.'3(1)) → _*4, rt ∈ Ω(n5)

Generator Equations:
_gen_nil':.'3(0) ⇔ nil'
_gen_nil':.'3(+(x, 1)) ⇔ .'(_gen_nil':.'3(x))

The following defined symbols remain to be analysed:
++'

Proved the following rewrite lemma:
++'(_gen_nil':.'3(_n13296), _gen_nil':.'3(b)) → _gen_nil':.'3(+(_n13296, b)), rt ∈ Ω(1 + n13296)

Induction Base:
++'(_gen_nil':.'3(0), _gen_nil':.'3(b)) →RΩ(1)
_gen_nil':.'3(b)

Induction Step:
++'(_gen_nil':.'3(+(_$n13297, 1)), _gen_nil':.'3(_b13459)) →RΩ(1)
.'(++'(_gen_nil':.'3(_$n13297), _gen_nil':.'3(_b13459))) →IH
.'(_gen_nil':.'3(+(_$n13297, _b13459)))

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

Rules:
merge'(nil', y) → y
merge'(x, nil') → x
merge'(.'(y), .'(v)) → if'(<', .'(merge'(y, .'(v))), .'(merge'(.'(y), v)))
++'(nil', y) → y
++'(.'(y), z) → .'(++'(y, z))
if'(true', x, y) → x
if'(false', x, y) → x

Types:
merge' :: nil':.' → nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.'
if' :: <':true':false' → nil':.' → nil':.' → nil':.'
<' :: <':true':false'
++' :: nil':.' → nil':.' → nil':.'
true' :: <':true':false'
false' :: <':true':false'
_hole_nil':.'1 :: nil':.'
_hole_<':true':false'2 :: <':true':false'
_gen_nil':.'3 :: Nat → nil':.'

Lemmas:
merge'(_gen_nil':.'3(+(1, _n5)), _gen_nil':.'3(1)) → _*4, rt ∈ Ω(n5)
++'(_gen_nil':.'3(_n13296), _gen_nil':.'3(b)) → _gen_nil':.'3(+(_n13296, b)), rt ∈ Ω(1 + n13296)

Generator Equations:
_gen_nil':.'3(0) ⇔ nil'
_gen_nil':.'3(+(x, 1)) ⇔ .'(_gen_nil':.'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
merge'(_gen_nil':.'3(+(1, _n5)), _gen_nil':.'3(1)) → _*4, rt ∈ Ω(n5)