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