eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
eq'(0', 0') → true'
eq'(0', s'(Y)) → false'
eq'(s'(X), 0') → false'
eq'(s'(X), s'(Y)) → eq'(X, Y)
le'(0', Y) → true'
le'(s'(X), 0') → false'
le'(s'(X), s'(Y)) → le'(X, Y)
min'(cons'(0', nil')) → 0'
min'(cons'(s'(N), nil')) → s'(N)
min'(cons'(N, cons'(M, L))) → ifmin'(le'(N, M), cons'(N, cons'(M, L)))
ifmin'(true', cons'(N, cons'(M, L))) → min'(cons'(N, L))
ifmin'(false', cons'(N, cons'(M, L))) → min'(cons'(M, L))
replace'(N, M, nil') → nil'
replace'(N, M, cons'(K, L)) → ifrepl'(eq'(N, K), N, M, cons'(K, L))
ifrepl'(true', N, M, cons'(K, L)) → cons'(M, L)
ifrepl'(false', N, M, cons'(K, L)) → cons'(K, replace'(N, M, L))
selsort'(nil') → nil'
selsort'(cons'(N, L)) → ifselsort'(eq'(N, min'(cons'(N, L))), cons'(N, L))
ifselsort'(true', cons'(N, L)) → cons'(N, selsort'(L))
ifselsort'(false', cons'(N, L)) → cons'(min'(cons'(N, L)), selsort'(replace'(min'(cons'(N, L)), N, L)))
Infered types.
Rules:
eq'(0', 0') → true'
eq'(0', s'(Y)) → false'
eq'(s'(X), 0') → false'
eq'(s'(X), s'(Y)) → eq'(X, Y)
le'(0', Y) → true'
le'(s'(X), 0') → false'
le'(s'(X), s'(Y)) → le'(X, Y)
min'(cons'(0', nil')) → 0'
min'(cons'(s'(N), nil')) → s'(N)
min'(cons'(N, cons'(M, L))) → ifmin'(le'(N, M), cons'(N, cons'(M, L)))
ifmin'(true', cons'(N, cons'(M, L))) → min'(cons'(N, L))
ifmin'(false', cons'(N, cons'(M, L))) → min'(cons'(M, L))
replace'(N, M, nil') → nil'
replace'(N, M, cons'(K, L)) → ifrepl'(eq'(N, K), N, M, cons'(K, L))
ifrepl'(true', N, M, cons'(K, L)) → cons'(M, L)
ifrepl'(false', N, M, cons'(K, L)) → cons'(K, replace'(N, M, L))
selsort'(nil') → nil'
selsort'(cons'(N, L)) → ifselsort'(eq'(N, min'(cons'(N, L))), cons'(N, L))
ifselsort'(true', cons'(N, L)) → cons'(N, selsort'(L))
ifselsort'(false', cons'(N, L)) → cons'(min'(cons'(N, L)), selsort'(replace'(min'(cons'(N, L)), N, L)))
Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
le' :: 0':s' → 0':s' → true':false'
min' :: nil':cons' → 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmin' :: true':false' → nil':cons' → 0':s'
replace' :: 0':s' → 0':s' → nil':cons' → nil':cons'
ifrepl' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
selsort' :: nil':cons' → nil':cons'
ifselsort' :: true':false' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':cons'3 :: nil':cons'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
eq', le', min', replace', selsort'
They will be analysed ascendingly in the following order:
eq' < replace'
eq' < selsort'
le' < min'
min' < selsort'
replace' < selsort'
Rules:
eq'(0', 0') → true'
eq'(0', s'(Y)) → false'
eq'(s'(X), 0') → false'
eq'(s'(X), s'(Y)) → eq'(X, Y)
le'(0', Y) → true'
le'(s'(X), 0') → false'
le'(s'(X), s'(Y)) → le'(X, Y)
min'(cons'(0', nil')) → 0'
min'(cons'(s'(N), nil')) → s'(N)
min'(cons'(N, cons'(M, L))) → ifmin'(le'(N, M), cons'(N, cons'(M, L)))
ifmin'(true', cons'(N, cons'(M, L))) → min'(cons'(N, L))
ifmin'(false', cons'(N, cons'(M, L))) → min'(cons'(M, L))
replace'(N, M, nil') → nil'
replace'(N, M, cons'(K, L)) → ifrepl'(eq'(N, K), N, M, cons'(K, L))
ifrepl'(true', N, M, cons'(K, L)) → cons'(M, L)
ifrepl'(false', N, M, cons'(K, L)) → cons'(K, replace'(N, M, L))
selsort'(nil') → nil'
selsort'(cons'(N, L)) → ifselsort'(eq'(N, min'(cons'(N, L))), cons'(N, L))
ifselsort'(true', cons'(N, L)) → cons'(N, selsort'(L))
ifselsort'(false', cons'(N, L)) → cons'(min'(cons'(N, L)), selsort'(replace'(min'(cons'(N, L)), N, L)))
Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
le' :: 0':s' → 0':s' → true':false'
min' :: nil':cons' → 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmin' :: true':false' → nil':cons' → 0':s'
replace' :: 0':s' → 0':s' → nil':cons' → nil':cons'
ifrepl' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
selsort' :: nil':cons' → nil':cons'
ifselsort' :: true':false' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':cons'3 :: nil':cons'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
eq', le', min', replace', selsort'
They will be analysed ascendingly in the following order:
eq' < replace'
eq' < selsort'
le' < min'
min' < selsort'
replace' < selsort'
Proved the following rewrite lemma:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
Induction Base:
eq'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
true'
Induction Step:
eq'(_gen_0':s'4(+(_$n8, 1)), _gen_0':s'4(+(_$n8, 1))) →RΩ(1)
eq'(_gen_0':s'4(_$n8), _gen_0':s'4(_$n8)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
eq'(0', 0') → true'
eq'(0', s'(Y)) → false'
eq'(s'(X), 0') → false'
eq'(s'(X), s'(Y)) → eq'(X, Y)
le'(0', Y) → true'
le'(s'(X), 0') → false'
le'(s'(X), s'(Y)) → le'(X, Y)
min'(cons'(0', nil')) → 0'
min'(cons'(s'(N), nil')) → s'(N)
min'(cons'(N, cons'(M, L))) → ifmin'(le'(N, M), cons'(N, cons'(M, L)))
ifmin'(true', cons'(N, cons'(M, L))) → min'(cons'(N, L))
ifmin'(false', cons'(N, cons'(M, L))) → min'(cons'(M, L))
replace'(N, M, nil') → nil'
replace'(N, M, cons'(K, L)) → ifrepl'(eq'(N, K), N, M, cons'(K, L))
ifrepl'(true', N, M, cons'(K, L)) → cons'(M, L)
ifrepl'(false', N, M, cons'(K, L)) → cons'(K, replace'(N, M, L))
selsort'(nil') → nil'
selsort'(cons'(N, L)) → ifselsort'(eq'(N, min'(cons'(N, L))), cons'(N, L))
ifselsort'(true', cons'(N, L)) → cons'(N, selsort'(L))
ifselsort'(false', cons'(N, L)) → cons'(min'(cons'(N, L)), selsort'(replace'(min'(cons'(N, L)), N, L)))
Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
le' :: 0':s' → 0':s' → true':false'
min' :: nil':cons' → 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmin' :: true':false' → nil':cons' → 0':s'
replace' :: 0':s' → 0':s' → nil':cons' → nil':cons'
ifrepl' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
selsort' :: nil':cons' → nil':cons'
ifselsort' :: true':false' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':cons'3 :: nil':cons'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
le', min', replace', selsort'
They will be analysed ascendingly in the following order:
le' < min'
min' < selsort'
replace' < selsort'
Proved the following rewrite lemma:
le'(_gen_0':s'4(_n1179), _gen_0':s'4(_n1179)) → true', rt ∈ Ω(1 + n1179)
Induction Base:
le'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
true'
Induction Step:
le'(_gen_0':s'4(+(_$n1180, 1)), _gen_0':s'4(+(_$n1180, 1))) →RΩ(1)
le'(_gen_0':s'4(_$n1180), _gen_0':s'4(_$n1180)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
eq'(0', 0') → true'
eq'(0', s'(Y)) → false'
eq'(s'(X), 0') → false'
eq'(s'(X), s'(Y)) → eq'(X, Y)
le'(0', Y) → true'
le'(s'(X), 0') → false'
le'(s'(X), s'(Y)) → le'(X, Y)
min'(cons'(0', nil')) → 0'
min'(cons'(s'(N), nil')) → s'(N)
min'(cons'(N, cons'(M, L))) → ifmin'(le'(N, M), cons'(N, cons'(M, L)))
ifmin'(true', cons'(N, cons'(M, L))) → min'(cons'(N, L))
ifmin'(false', cons'(N, cons'(M, L))) → min'(cons'(M, L))
replace'(N, M, nil') → nil'
replace'(N, M, cons'(K, L)) → ifrepl'(eq'(N, K), N, M, cons'(K, L))
ifrepl'(true', N, M, cons'(K, L)) → cons'(M, L)
ifrepl'(false', N, M, cons'(K, L)) → cons'(K, replace'(N, M, L))
selsort'(nil') → nil'
selsort'(cons'(N, L)) → ifselsort'(eq'(N, min'(cons'(N, L))), cons'(N, L))
ifselsort'(true', cons'(N, L)) → cons'(N, selsort'(L))
ifselsort'(false', cons'(N, L)) → cons'(min'(cons'(N, L)), selsort'(replace'(min'(cons'(N, L)), N, L)))
Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
le' :: 0':s' → 0':s' → true':false'
min' :: nil':cons' → 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmin' :: true':false' → nil':cons' → 0':s'
replace' :: 0':s' → 0':s' → nil':cons' → nil':cons'
ifrepl' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
selsort' :: nil':cons' → nil':cons'
ifselsort' :: true':false' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':cons'3 :: nil':cons'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1179), _gen_0':s'4(_n1179)) → true', rt ∈ Ω(1 + n1179)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
min', replace', selsort'
They will be analysed ascendingly in the following order:
min' < selsort'
replace' < selsort'
Proved the following rewrite lemma:
min'(_gen_nil':cons'5(+(1, _n2269))) → _gen_0':s'4(0), rt ∈ Ω(1 + n2269)
Induction Base:
min'(_gen_nil':cons'5(+(1, 0))) →RΩ(1)
0'
Induction Step:
min'(_gen_nil':cons'5(+(1, +(_$n2270, 1)))) →RΩ(1)
ifmin'(le'(0', 0'), cons'(0', cons'(0', _gen_nil':cons'5(_$n2270)))) →LΩ(1)
ifmin'(true', cons'(0', cons'(0', _gen_nil':cons'5(_$n2270)))) →RΩ(1)
min'(cons'(0', _gen_nil':cons'5(_$n2270))) →IH
_gen_0':s'4(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
eq'(0', 0') → true'
eq'(0', s'(Y)) → false'
eq'(s'(X), 0') → false'
eq'(s'(X), s'(Y)) → eq'(X, Y)
le'(0', Y) → true'
le'(s'(X), 0') → false'
le'(s'(X), s'(Y)) → le'(X, Y)
min'(cons'(0', nil')) → 0'
min'(cons'(s'(N), nil')) → s'(N)
min'(cons'(N, cons'(M, L))) → ifmin'(le'(N, M), cons'(N, cons'(M, L)))
ifmin'(true', cons'(N, cons'(M, L))) → min'(cons'(N, L))
ifmin'(false', cons'(N, cons'(M, L))) → min'(cons'(M, L))
replace'(N, M, nil') → nil'
replace'(N, M, cons'(K, L)) → ifrepl'(eq'(N, K), N, M, cons'(K, L))
ifrepl'(true', N, M, cons'(K, L)) → cons'(M, L)
ifrepl'(false', N, M, cons'(K, L)) → cons'(K, replace'(N, M, L))
selsort'(nil') → nil'
selsort'(cons'(N, L)) → ifselsort'(eq'(N, min'(cons'(N, L))), cons'(N, L))
ifselsort'(true', cons'(N, L)) → cons'(N, selsort'(L))
ifselsort'(false', cons'(N, L)) → cons'(min'(cons'(N, L)), selsort'(replace'(min'(cons'(N, L)), N, L)))
Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
le' :: 0':s' → 0':s' → true':false'
min' :: nil':cons' → 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmin' :: true':false' → nil':cons' → 0':s'
replace' :: 0':s' → 0':s' → nil':cons' → nil':cons'
ifrepl' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
selsort' :: nil':cons' → nil':cons'
ifselsort' :: true':false' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':cons'3 :: nil':cons'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1179), _gen_0':s'4(_n1179)) → true', rt ∈ Ω(1 + n1179)
min'(_gen_nil':cons'5(+(1, _n2269))) → _gen_0':s'4(0), rt ∈ Ω(1 + n2269)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
replace', selsort'
They will be analysed ascendingly in the following order:
replace' < selsort'
Could not prove a rewrite lemma for the defined symbol replace'.
Rules:
eq'(0', 0') → true'
eq'(0', s'(Y)) → false'
eq'(s'(X), 0') → false'
eq'(s'(X), s'(Y)) → eq'(X, Y)
le'(0', Y) → true'
le'(s'(X), 0') → false'
le'(s'(X), s'(Y)) → le'(X, Y)
min'(cons'(0', nil')) → 0'
min'(cons'(s'(N), nil')) → s'(N)
min'(cons'(N, cons'(M, L))) → ifmin'(le'(N, M), cons'(N, cons'(M, L)))
ifmin'(true', cons'(N, cons'(M, L))) → min'(cons'(N, L))
ifmin'(false', cons'(N, cons'(M, L))) → min'(cons'(M, L))
replace'(N, M, nil') → nil'
replace'(N, M, cons'(K, L)) → ifrepl'(eq'(N, K), N, M, cons'(K, L))
ifrepl'(true', N, M, cons'(K, L)) → cons'(M, L)
ifrepl'(false', N, M, cons'(K, L)) → cons'(K, replace'(N, M, L))
selsort'(nil') → nil'
selsort'(cons'(N, L)) → ifselsort'(eq'(N, min'(cons'(N, L))), cons'(N, L))
ifselsort'(true', cons'(N, L)) → cons'(N, selsort'(L))
ifselsort'(false', cons'(N, L)) → cons'(min'(cons'(N, L)), selsort'(replace'(min'(cons'(N, L)), N, L)))
Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
le' :: 0':s' → 0':s' → true':false'
min' :: nil':cons' → 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmin' :: true':false' → nil':cons' → 0':s'
replace' :: 0':s' → 0':s' → nil':cons' → nil':cons'
ifrepl' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
selsort' :: nil':cons' → nil':cons'
ifselsort' :: true':false' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':cons'3 :: nil':cons'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1179), _gen_0':s'4(_n1179)) → true', rt ∈ Ω(1 + n1179)
min'(_gen_nil':cons'5(+(1, _n2269))) → _gen_0':s'4(0), rt ∈ Ω(1 + n2269)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
selsort'
Proved the following rewrite lemma:
selsort'(_gen_nil':cons'5(_n5080)) → _gen_nil':cons'5(_n5080), rt ∈ Ω(1 + n5080 + n50802)
Induction Base:
selsort'(_gen_nil':cons'5(0)) →RΩ(1)
nil'
Induction Step:
selsort'(_gen_nil':cons'5(+(_$n5081, 1))) →RΩ(1)
ifselsort'(eq'(0', min'(cons'(0', _gen_nil':cons'5(_$n5081)))), cons'(0', _gen_nil':cons'5(_$n5081))) →LΩ(1 + $n5081)
ifselsort'(eq'(0', _gen_0':s'4(0)), cons'(0', _gen_nil':cons'5(_$n5081))) →LΩ(1)
ifselsort'(true', cons'(0', _gen_nil':cons'5(_$n5081))) →RΩ(1)
cons'(0', selsort'(_gen_nil':cons'5(_$n5081))) →IH
cons'(0', _gen_nil':cons'5(_$n5081))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
eq'(0', 0') → true'
eq'(0', s'(Y)) → false'
eq'(s'(X), 0') → false'
eq'(s'(X), s'(Y)) → eq'(X, Y)
le'(0', Y) → true'
le'(s'(X), 0') → false'
le'(s'(X), s'(Y)) → le'(X, Y)
min'(cons'(0', nil')) → 0'
min'(cons'(s'(N), nil')) → s'(N)
min'(cons'(N, cons'(M, L))) → ifmin'(le'(N, M), cons'(N, cons'(M, L)))
ifmin'(true', cons'(N, cons'(M, L))) → min'(cons'(N, L))
ifmin'(false', cons'(N, cons'(M, L))) → min'(cons'(M, L))
replace'(N, M, nil') → nil'
replace'(N, M, cons'(K, L)) → ifrepl'(eq'(N, K), N, M, cons'(K, L))
ifrepl'(true', N, M, cons'(K, L)) → cons'(M, L)
ifrepl'(false', N, M, cons'(K, L)) → cons'(K, replace'(N, M, L))
selsort'(nil') → nil'
selsort'(cons'(N, L)) → ifselsort'(eq'(N, min'(cons'(N, L))), cons'(N, L))
ifselsort'(true', cons'(N, L)) → cons'(N, selsort'(L))
ifselsort'(false', cons'(N, L)) → cons'(min'(cons'(N, L)), selsort'(replace'(min'(cons'(N, L)), N, L)))
Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
le' :: 0':s' → 0':s' → true':false'
min' :: nil':cons' → 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmin' :: true':false' → nil':cons' → 0':s'
replace' :: 0':s' → 0':s' → nil':cons' → nil':cons'
ifrepl' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
selsort' :: nil':cons' → nil':cons'
ifselsort' :: true':false' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':cons'3 :: nil':cons'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1179), _gen_0':s'4(_n1179)) → true', rt ∈ Ω(1 + n1179)
min'(_gen_nil':cons'5(+(1, _n2269))) → _gen_0':s'4(0), rt ∈ Ω(1 + n2269)
selsort'(_gen_nil':cons'5(_n5080)) → _gen_nil':cons'5(_n5080), rt ∈ Ω(1 + n5080 + n50802)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
selsort'(_gen_nil':cons'5(_n5080)) → _gen_nil':cons'5(_n5080), rt ∈ Ω(1 + n5080 + n50802)