sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
sort'(l) → st'(0', l)
st'(n, l) → cond1'(member'(n, l), n, l)
cond1'(true', n, l) → cons'(n, st'(s'(n), l))
cond1'(false', n, l) → cond2'(gt'(n, max'(l)), n, l)
cond2'(true', n, l) → nil'
cond2'(false', n, l) → st'(s'(n), l)
member'(n, nil') → false'
member'(n, cons'(m, l)) → or'(equal'(n, m), member'(n, l))
or'(x, true') → true'
or'(x, false') → x
equal'(0', 0') → true'
equal'(s'(x), 0') → false'
equal'(0', s'(y)) → false'
equal'(s'(x), s'(y)) → equal'(x, y)
gt'(0', v) → false'
gt'(s'(u), 0') → true'
gt'(s'(u), s'(v)) → gt'(u, v)
max'(nil') → 0'
max'(cons'(u, l)) → if'(gt'(u, max'(l)), u, max'(l))
if'(true', u, v) → u
if'(false', u, v) → v
Infered types.
Rules:
sort'(l) → st'(0', l)
st'(n, l) → cond1'(member'(n, l), n, l)
cond1'(true', n, l) → cons'(n, st'(s'(n), l))
cond1'(false', n, l) → cond2'(gt'(n, max'(l)), n, l)
cond2'(true', n, l) → nil'
cond2'(false', n, l) → st'(s'(n), l)
member'(n, nil') → false'
member'(n, cons'(m, l)) → or'(equal'(n, m), member'(n, l))
or'(x, true') → true'
or'(x, false') → x
equal'(0', 0') → true'
equal'(s'(x), 0') → false'
equal'(0', s'(y)) → false'
equal'(s'(x), s'(y)) → equal'(x, y)
gt'(0', v) → false'
gt'(s'(u), 0') → true'
gt'(s'(u), s'(v)) → gt'(u, v)
max'(nil') → 0'
max'(cons'(u, l)) → if'(gt'(u, max'(l)), u, max'(l))
if'(true', u, v) → u
if'(false', u, v) → v
Types:
sort' :: cons':nil' → cons':nil'
st' :: 0':s' → cons':nil' → cons':nil'
0' :: 0':s'
cond1' :: true':false' → 0':s' → cons':nil' → cons':nil'
member' :: 0':s' → cons':nil' → true':false'
true' :: true':false'
cons' :: 0':s' → cons':nil' → cons':nil'
s' :: 0':s' → 0':s'
false' :: true':false'
cond2' :: true':false' → 0':s' → cons':nil' → cons':nil'
gt' :: 0':s' → 0':s' → true':false'
max' :: cons':nil' → 0':s'
nil' :: cons':nil'
or' :: true':false' → true':false' → true':false'
equal' :: 0':s' → 0':s' → true':false'
if' :: true':false' → 0':s' → 0':s' → 0':s'
_hole_cons':nil'1 :: cons':nil'
_hole_0':s'2 :: 0':s'
_hole_true':false'3 :: true':false'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
st', member', gt', max', equal'
They will be analysed ascendingly in the following order:
member' < st'
gt' < st'
max' < st'
equal' < member'
gt' < max'
Rules:
sort'(l) → st'(0', l)
st'(n, l) → cond1'(member'(n, l), n, l)
cond1'(true', n, l) → cons'(n, st'(s'(n), l))
cond1'(false', n, l) → cond2'(gt'(n, max'(l)), n, l)
cond2'(true', n, l) → nil'
cond2'(false', n, l) → st'(s'(n), l)
member'(n, nil') → false'
member'(n, cons'(m, l)) → or'(equal'(n, m), member'(n, l))
or'(x, true') → true'
or'(x, false') → x
equal'(0', 0') → true'
equal'(s'(x), 0') → false'
equal'(0', s'(y)) → false'
equal'(s'(x), s'(y)) → equal'(x, y)
gt'(0', v) → false'
gt'(s'(u), 0') → true'
gt'(s'(u), s'(v)) → gt'(u, v)
max'(nil') → 0'
max'(cons'(u, l)) → if'(gt'(u, max'(l)), u, max'(l))
if'(true', u, v) → u
if'(false', u, v) → v
Types:
sort' :: cons':nil' → cons':nil'
st' :: 0':s' → cons':nil' → cons':nil'
0' :: 0':s'
cond1' :: true':false' → 0':s' → cons':nil' → cons':nil'
member' :: 0':s' → cons':nil' → true':false'
true' :: true':false'
cons' :: 0':s' → cons':nil' → cons':nil'
s' :: 0':s' → 0':s'
false' :: true':false'
cond2' :: true':false' → 0':s' → cons':nil' → cons':nil'
gt' :: 0':s' → 0':s' → true':false'
max' :: cons':nil' → 0':s'
nil' :: cons':nil'
or' :: true':false' → true':false' → true':false'
equal' :: 0':s' → 0':s' → true':false'
if' :: true':false' → 0':s' → 0':s' → 0':s'
_hole_cons':nil'1 :: cons':nil'
_hole_0':s'2 :: 0':s'
_hole_true':false'3 :: true':false'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'
Generator Equations:
_gen_cons':nil'4(0) ⇔ nil'
_gen_cons':nil'4(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
The following defined symbols remain to be analysed:
gt', st', member', max', equal'
They will be analysed ascendingly in the following order:
member' < st'
gt' < st'
max' < st'
equal' < member'
gt' < max'
Proved the following rewrite lemma:
gt'(_gen_0':s'5(_n7), _gen_0':s'5(_n7)) → false', rt ∈ Ω(1 + n7)
Induction Base:
gt'(_gen_0':s'5(0), _gen_0':s'5(0)) →RΩ(1)
false'
Induction Step:
gt'(_gen_0':s'5(+(_$n8, 1)), _gen_0':s'5(+(_$n8, 1))) →RΩ(1)
gt'(_gen_0':s'5(_$n8), _gen_0':s'5(_$n8)) →IH
false'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
sort'(l) → st'(0', l)
st'(n, l) → cond1'(member'(n, l), n, l)
cond1'(true', n, l) → cons'(n, st'(s'(n), l))
cond1'(false', n, l) → cond2'(gt'(n, max'(l)), n, l)
cond2'(true', n, l) → nil'
cond2'(false', n, l) → st'(s'(n), l)
member'(n, nil') → false'
member'(n, cons'(m, l)) → or'(equal'(n, m), member'(n, l))
or'(x, true') → true'
or'(x, false') → x
equal'(0', 0') → true'
equal'(s'(x), 0') → false'
equal'(0', s'(y)) → false'
equal'(s'(x), s'(y)) → equal'(x, y)
gt'(0', v) → false'
gt'(s'(u), 0') → true'
gt'(s'(u), s'(v)) → gt'(u, v)
max'(nil') → 0'
max'(cons'(u, l)) → if'(gt'(u, max'(l)), u, max'(l))
if'(true', u, v) → u
if'(false', u, v) → v
Types:
sort' :: cons':nil' → cons':nil'
st' :: 0':s' → cons':nil' → cons':nil'
0' :: 0':s'
cond1' :: true':false' → 0':s' → cons':nil' → cons':nil'
member' :: 0':s' → cons':nil' → true':false'
true' :: true':false'
cons' :: 0':s' → cons':nil' → cons':nil'
s' :: 0':s' → 0':s'
false' :: true':false'
cond2' :: true':false' → 0':s' → cons':nil' → cons':nil'
gt' :: 0':s' → 0':s' → true':false'
max' :: cons':nil' → 0':s'
nil' :: cons':nil'
or' :: true':false' → true':false' → true':false'
equal' :: 0':s' → 0':s' → true':false'
if' :: true':false' → 0':s' → 0':s' → 0':s'
_hole_cons':nil'1 :: cons':nil'
_hole_0':s'2 :: 0':s'
_hole_true':false'3 :: true':false'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
gt'(_gen_0':s'5(_n7), _gen_0':s'5(_n7)) → false', rt ∈ Ω(1 + n7)
Generator Equations:
_gen_cons':nil'4(0) ⇔ nil'
_gen_cons':nil'4(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
The following defined symbols remain to be analysed:
max', st', member', equal'
They will be analysed ascendingly in the following order:
member' < st'
max' < st'
equal' < member'
Proved the following rewrite lemma:
max'(_gen_cons':nil'4(_n923)) → _gen_0':s'5(0), rt ∈ Ω(2n)
Induction Base:
max'(_gen_cons':nil'4(0)) →RΩ(1)
0'
Induction Step:
max'(_gen_cons':nil'4(+(_$n924, 1))) →RΩ(1)
if'(gt'(0', max'(_gen_cons':nil'4(_$n924))), 0', max'(_gen_cons':nil'4(_$n924))) →IH
if'(gt'(0', _gen_0':s'5(0)), 0', max'(_gen_cons':nil'4(_$n924))) →LΩ(1)
if'(false', 0', max'(_gen_cons':nil'4(_$n924))) →IH
if'(false', 0', _gen_0':s'5(0)) →RΩ(1)
_gen_0':s'5(0)
We have rt ∈ Ω(2n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(2n)