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

msort(nil) → nil
msort(.(x, y)) → .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) → x
min(x, .(y, z)) → if(<=(x, y), min(x, z), min(y, z))
del(x, nil) → nil
del(x, .(y, z)) → if(=(x, y), z, .(y, del(x, z)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

msort'(nil') → nil'
msort'(.'(x, y)) → .'(min'(x, y), msort'(del'(min'(x, y), .'(x, y))))
min'(x, nil') → x
min'(x, .'(y, z)) → if'(<='(x, y), min'(x, z), min'(y, z))
del'(x, nil') → nil'
del'(x, .'(y, z)) → if'(='(x, y), z, .'(y, del'(x, z)))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
if'/0
<='/0
<='/1
='/0
='/1

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

msort'(nil') → nil'
msort'(.'(x, y)) → .'(min'(x, y), msort'(del'(min'(x, y), .'(x, y))))
min'(x, nil') → x
min'(x, .'(y, z)) → if'(min'(x, z), min'(y, z))
del'(x, nil') → nil'
del'(x, .'(y, z)) → if'(z, .'(y, del'(x, z)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
msort'(nil') → nil'
msort'(.'(x, y)) → .'(min'(x, y), msort'(del'(min'(x, y), .'(x, y))))
min'(x, nil') → x
min'(x, .'(y, z)) → if'(min'(x, z), min'(y, z))
del'(x, nil') → nil'
del'(x, .'(y, z)) → if'(z, .'(y, del'(x, z)))

Types:
msort' :: nil':.':if' → nil':.':if'
nil' :: nil':.':if'
.' :: nil':.':if' → nil':.':if' → nil':.':if'
min' :: nil':.':if' → nil':.':if' → nil':.':if'
del' :: nil':.':if' → nil':.':if' → nil':.':if'
if' :: nil':.':if' → nil':.':if' → nil':.':if'
_hole_nil':.':if'1 :: nil':.':if'
_gen_nil':.':if'2 :: Nat → nil':.':if'

Heuristically decided to analyse the following defined symbols:
msort', min', del'

They will be analysed ascendingly in the following order:
min' < msort'
del' < msort'

Rules:
msort'(nil') → nil'
msort'(.'(x, y)) → .'(min'(x, y), msort'(del'(min'(x, y), .'(x, y))))
min'(x, nil') → x
min'(x, .'(y, z)) → if'(min'(x, z), min'(y, z))
del'(x, nil') → nil'
del'(x, .'(y, z)) → if'(z, .'(y, del'(x, z)))

Types:
msort' :: nil':.':if' → nil':.':if'
nil' :: nil':.':if'
.' :: nil':.':if' → nil':.':if' → nil':.':if'
min' :: nil':.':if' → nil':.':if' → nil':.':if'
del' :: nil':.':if' → nil':.':if' → nil':.':if'
if' :: nil':.':if' → nil':.':if' → nil':.':if'
_hole_nil':.':if'1 :: nil':.':if'
_gen_nil':.':if'2 :: Nat → nil':.':if'

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

The following defined symbols remain to be analysed:
min', msort', del'

They will be analysed ascendingly in the following order:
min' < msort'
del' < msort'

Proved the following rewrite lemma:
min'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

Induction Base:
min'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, 0)))

Induction Step:
min'(_gen_nil':.':if'2(_a12262), _gen_nil':.':if'2(+(1, +(_\$n5, 1)))) →RΩ(1)
if'(min'(_gen_nil':.':if'2(_a12262), _gen_nil':.':if'2(+(1, _\$n5))), min'(nil', _gen_nil':.':if'2(+(1, _\$n5)))) →IH
if'(_*3, min'(nil', _gen_nil':.':if'2(+(1, _\$n5)))) →RΩ(1)
if'(_*3, if'(min'(nil', _gen_nil':.':if'2(_\$n5)), min'(nil', _gen_nil':.':if'2(_\$n5))))

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

Rules:
msort'(nil') → nil'
msort'(.'(x, y)) → .'(min'(x, y), msort'(del'(min'(x, y), .'(x, y))))
min'(x, nil') → x
min'(x, .'(y, z)) → if'(min'(x, z), min'(y, z))
del'(x, nil') → nil'
del'(x, .'(y, z)) → if'(z, .'(y, del'(x, z)))

Types:
msort' :: nil':.':if' → nil':.':if'
nil' :: nil':.':if'
.' :: nil':.':if' → nil':.':if' → nil':.':if'
min' :: nil':.':if' → nil':.':if' → nil':.':if'
del' :: nil':.':if' → nil':.':if' → nil':.':if'
if' :: nil':.':if' → nil':.':if' → nil':.':if'
_hole_nil':.':if'1 :: nil':.':if'
_gen_nil':.':if'2 :: Nat → nil':.':if'

Lemmas:
min'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

The following defined symbols remain to be analysed:
del', msort'

They will be analysed ascendingly in the following order:
del' < msort'

Proved the following rewrite lemma:
del'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, _n12689))) → _*3, rt ∈ Ω(n12689)

Induction Base:
del'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, 0)))

Induction Step:
del'(_gen_nil':.':if'2(_a36350), _gen_nil':.':if'2(+(1, +(_\$n12690, 1)))) →RΩ(1)
if'(_gen_nil':.':if'2(+(1, _\$n12690)), .'(nil', del'(_gen_nil':.':if'2(_a36350), _gen_nil':.':if'2(+(1, _\$n12690))))) →IH
if'(_gen_nil':.':if'2(+(1, _\$n12690)), .'(nil', _*3))

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

Rules:
msort'(nil') → nil'
msort'(.'(x, y)) → .'(min'(x, y), msort'(del'(min'(x, y), .'(x, y))))
min'(x, nil') → x
min'(x, .'(y, z)) → if'(min'(x, z), min'(y, z))
del'(x, nil') → nil'
del'(x, .'(y, z)) → if'(z, .'(y, del'(x, z)))

Types:
msort' :: nil':.':if' → nil':.':if'
nil' :: nil':.':if'
.' :: nil':.':if' → nil':.':if' → nil':.':if'
min' :: nil':.':if' → nil':.':if' → nil':.':if'
del' :: nil':.':if' → nil':.':if' → nil':.':if'
if' :: nil':.':if' → nil':.':if' → nil':.':if'
_hole_nil':.':if'1 :: nil':.':if'
_gen_nil':.':if'2 :: Nat → nil':.':if'

Lemmas:
min'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
del'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, _n12689))) → _*3, rt ∈ Ω(n12689)

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

The following defined symbols remain to be analysed:
msort'

Could not prove a rewrite lemma for the defined symbol msort'.

Rules:
msort'(nil') → nil'
msort'(.'(x, y)) → .'(min'(x, y), msort'(del'(min'(x, y), .'(x, y))))
min'(x, nil') → x
min'(x, .'(y, z)) → if'(min'(x, z), min'(y, z))
del'(x, nil') → nil'
del'(x, .'(y, z)) → if'(z, .'(y, del'(x, z)))

Types:
msort' :: nil':.':if' → nil':.':if'
nil' :: nil':.':if'
.' :: nil':.':if' → nil':.':if' → nil':.':if'
min' :: nil':.':if' → nil':.':if' → nil':.':if'
del' :: nil':.':if' → nil':.':if' → nil':.':if'
if' :: nil':.':if' → nil':.':if' → nil':.':if'
_hole_nil':.':if'1 :: nil':.':if'
_gen_nil':.':if'2 :: Nat → nil':.':if'

Lemmas:
min'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
del'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, _n12689))) → _*3, rt ∈ Ω(n12689)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
min'(_gen_nil':.':if'2(a), _gen_nil':.':if'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)