le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, add'(m, x)) → if_low'(le'(m, n), n, add'(m, x))
if_low'(true', n, add'(m, x)) → add'(m, low'(n, x))
if_low'(false', n, add'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, add'(m, x)) → if_high'(le'(m, n), n, add'(m, x))
if_high'(true', n, add'(m, x)) → high'(n, x)
if_high'(false', n, add'(m, x)) → add'(m, high'(n, x))
head'(add'(n, x)) → n
tail'(add'(n, x)) → x
isempty'(nil') → true'
isempty'(add'(n, x)) → false'
quicksort'(x) → if_qs'(isempty'(x), low'(head'(x), tail'(x)), head'(x), high'(head'(x), tail'(x)))
if_qs'(true', x, n, y) → nil'
if_qs'(false', x, n, y) → app'(quicksort'(x), add'(n, quicksort'(y)))
Infered types.
Rules:
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, add'(m, x)) → if_low'(le'(m, n), n, add'(m, x))
if_low'(true', n, add'(m, x)) → add'(m, low'(n, x))
if_low'(false', n, add'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, add'(m, x)) → if_high'(le'(m, n), n, add'(m, x))
if_high'(true', n, add'(m, x)) → high'(n, x)
if_high'(false', n, add'(m, x)) → add'(m, high'(n, x))
head'(add'(n, x)) → n
tail'(add'(n, x)) → x
isempty'(nil') → true'
isempty'(add'(n, x)) → false'
quicksort'(x) → if_qs'(isempty'(x), low'(head'(x), tail'(x)), head'(x), high'(head'(x), tail'(x)))
if_qs'(true', x, n, y) → nil'
if_qs'(false', x, n, y) → app'(quicksort'(x), add'(n, quicksort'(y)))
Types:
le' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: 0':s' → nil':add' → nil':add'
low' :: 0':s' → nil':add' → nil':add'
if_low' :: true':false' → 0':s' → nil':add' → nil':add'
high' :: 0':s' → nil':add' → nil':add'
if_high' :: true':false' → 0':s' → nil':add' → nil':add'
head' :: nil':add' → 0':s'
tail' :: nil':add' → nil':add'
isempty' :: nil':add' → true':false'
quicksort' :: nil':add' → nil':add'
if_qs' :: true':false' → nil':add' → 0':s' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Heuristically decided to analyse the following defined symbols:
le', app', low', high', quicksort'
They will be analysed ascendingly in the following order:
le' < low'
le' < high'
app' < quicksort'
low' < quicksort'
high' < quicksort'
Rules:
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, add'(m, x)) → if_low'(le'(m, n), n, add'(m, x))
if_low'(true', n, add'(m, x)) → add'(m, low'(n, x))
if_low'(false', n, add'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, add'(m, x)) → if_high'(le'(m, n), n, add'(m, x))
if_high'(true', n, add'(m, x)) → high'(n, x)
if_high'(false', n, add'(m, x)) → add'(m, high'(n, x))
head'(add'(n, x)) → n
tail'(add'(n, x)) → x
isempty'(nil') → true'
isempty'(add'(n, x)) → false'
quicksort'(x) → if_qs'(isempty'(x), low'(head'(x), tail'(x)), head'(x), high'(head'(x), tail'(x)))
if_qs'(true', x, n, y) → nil'
if_qs'(false', x, n, y) → app'(quicksort'(x), add'(n, quicksort'(y)))
Types:
le' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: 0':s' → nil':add' → nil':add'
low' :: 0':s' → nil':add' → nil':add'
if_low' :: true':false' → 0':s' → nil':add' → nil':add'
high' :: 0':s' → nil':add' → nil':add'
if_high' :: true':false' → 0':s' → nil':add' → nil':add'
head' :: nil':add' → 0':s'
tail' :: nil':add' → nil':add'
isempty' :: nil':add' → true':false'
quicksort' :: nil':add' → nil':add'
if_qs' :: true':false' → nil':add' → 0':s' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':add'5(0) ⇔ nil'
_gen_nil':add'5(+(x, 1)) ⇔ add'(0', _gen_nil':add'5(x))
The following defined symbols remain to be analysed:
le', app', low', high', quicksort'
They will be analysed ascendingly in the following order:
le' < low'
le' < high'
app' < quicksort'
low' < quicksort'
high' < quicksort'
Proved the following rewrite lemma:
le'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
Induction Base:
le'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
true'
Induction Step:
le'(_gen_0':s'4(+(_$n8, 1)), _gen_0':s'4(+(_$n8, 1))) →RΩ(1)
le'(_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:
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, add'(m, x)) → if_low'(le'(m, n), n, add'(m, x))
if_low'(true', n, add'(m, x)) → add'(m, low'(n, x))
if_low'(false', n, add'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, add'(m, x)) → if_high'(le'(m, n), n, add'(m, x))
if_high'(true', n, add'(m, x)) → high'(n, x)
if_high'(false', n, add'(m, x)) → add'(m, high'(n, x))
head'(add'(n, x)) → n
tail'(add'(n, x)) → x
isempty'(nil') → true'
isempty'(add'(n, x)) → false'
quicksort'(x) → if_qs'(isempty'(x), low'(head'(x), tail'(x)), head'(x), high'(head'(x), tail'(x)))
if_qs'(true', x, n, y) → nil'
if_qs'(false', x, n, y) → app'(quicksort'(x), add'(n, quicksort'(y)))
Types:
le' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: 0':s' → nil':add' → nil':add'
low' :: 0':s' → nil':add' → nil':add'
if_low' :: true':false' → 0':s' → nil':add' → nil':add'
high' :: 0':s' → nil':add' → nil':add'
if_high' :: true':false' → 0':s' → nil':add' → nil':add'
head' :: nil':add' → 0':s'
tail' :: nil':add' → nil':add'
isempty' :: nil':add' → true':false'
quicksort' :: nil':add' → nil':add'
if_qs' :: true':false' → nil':add' → 0':s' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
le'(_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':add'5(0) ⇔ nil'
_gen_nil':add'5(+(x, 1)) ⇔ add'(0', _gen_nil':add'5(x))
The following defined symbols remain to be analysed:
app', low', high', quicksort'
They will be analysed ascendingly in the following order:
app' < quicksort'
low' < quicksort'
high' < quicksort'
Proved the following rewrite lemma:
app'(_gen_nil':add'5(_n1109), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n1109, b)), rt ∈ Ω(1 + n1109)
Induction Base:
app'(_gen_nil':add'5(0), _gen_nil':add'5(b)) →RΩ(1)
_gen_nil':add'5(b)
Induction Step:
app'(_gen_nil':add'5(+(_$n1110, 1)), _gen_nil':add'5(_b1340)) →RΩ(1)
add'(0', app'(_gen_nil':add'5(_$n1110), _gen_nil':add'5(_b1340))) →IH
add'(0', _gen_nil':add'5(+(_$n1110, _b1340)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, add'(m, x)) → if_low'(le'(m, n), n, add'(m, x))
if_low'(true', n, add'(m, x)) → add'(m, low'(n, x))
if_low'(false', n, add'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, add'(m, x)) → if_high'(le'(m, n), n, add'(m, x))
if_high'(true', n, add'(m, x)) → high'(n, x)
if_high'(false', n, add'(m, x)) → add'(m, high'(n, x))
head'(add'(n, x)) → n
tail'(add'(n, x)) → x
isempty'(nil') → true'
isempty'(add'(n, x)) → false'
quicksort'(x) → if_qs'(isempty'(x), low'(head'(x), tail'(x)), head'(x), high'(head'(x), tail'(x)))
if_qs'(true', x, n, y) → nil'
if_qs'(false', x, n, y) → app'(quicksort'(x), add'(n, quicksort'(y)))
Types:
le' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: 0':s' → nil':add' → nil':add'
low' :: 0':s' → nil':add' → nil':add'
if_low' :: true':false' → 0':s' → nil':add' → nil':add'
high' :: 0':s' → nil':add' → nil':add'
if_high' :: true':false' → 0':s' → nil':add' → nil':add'
head' :: nil':add' → 0':s'
tail' :: nil':add' → nil':add'
isempty' :: nil':add' → true':false'
quicksort' :: nil':add' → nil':add'
if_qs' :: true':false' → nil':add' → 0':s' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
le'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
app'(_gen_nil':add'5(_n1109), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n1109, b)), rt ∈ Ω(1 + n1109)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':add'5(0) ⇔ nil'
_gen_nil':add'5(+(x, 1)) ⇔ add'(0', _gen_nil':add'5(x))
The following defined symbols remain to be analysed:
low', high', quicksort'
They will be analysed ascendingly in the following order:
low' < quicksort'
high' < quicksort'
Proved the following rewrite lemma:
low'(_gen_0':s'4(0), _gen_nil':add'5(_n2747)) → _gen_nil':add'5(_n2747), rt ∈ Ω(1 + n2747)
Induction Base:
low'(_gen_0':s'4(0), _gen_nil':add'5(0)) →RΩ(1)
nil'
Induction Step:
low'(_gen_0':s'4(0), _gen_nil':add'5(+(_$n2748, 1))) →RΩ(1)
if_low'(le'(0', _gen_0':s'4(0)), _gen_0':s'4(0), add'(0', _gen_nil':add'5(_$n2748))) →LΩ(1)
if_low'(true', _gen_0':s'4(0), add'(0', _gen_nil':add'5(_$n2748))) →RΩ(1)
add'(0', low'(_gen_0':s'4(0), _gen_nil':add'5(_$n2748))) →IH
add'(0', _gen_nil':add'5(_$n2748))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, add'(m, x)) → if_low'(le'(m, n), n, add'(m, x))
if_low'(true', n, add'(m, x)) → add'(m, low'(n, x))
if_low'(false', n, add'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, add'(m, x)) → if_high'(le'(m, n), n, add'(m, x))
if_high'(true', n, add'(m, x)) → high'(n, x)
if_high'(false', n, add'(m, x)) → add'(m, high'(n, x))
head'(add'(n, x)) → n
tail'(add'(n, x)) → x
isempty'(nil') → true'
isempty'(add'(n, x)) → false'
quicksort'(x) → if_qs'(isempty'(x), low'(head'(x), tail'(x)), head'(x), high'(head'(x), tail'(x)))
if_qs'(true', x, n, y) → nil'
if_qs'(false', x, n, y) → app'(quicksort'(x), add'(n, quicksort'(y)))
Types:
le' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: 0':s' → nil':add' → nil':add'
low' :: 0':s' → nil':add' → nil':add'
if_low' :: true':false' → 0':s' → nil':add' → nil':add'
high' :: 0':s' → nil':add' → nil':add'
if_high' :: true':false' → 0':s' → nil':add' → nil':add'
head' :: nil':add' → 0':s'
tail' :: nil':add' → nil':add'
isempty' :: nil':add' → true':false'
quicksort' :: nil':add' → nil':add'
if_qs' :: true':false' → nil':add' → 0':s' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
le'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
app'(_gen_nil':add'5(_n1109), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n1109, b)), rt ∈ Ω(1 + n1109)
low'(_gen_0':s'4(0), _gen_nil':add'5(_n2747)) → _gen_nil':add'5(_n2747), rt ∈ Ω(1 + n2747)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':add'5(0) ⇔ nil'
_gen_nil':add'5(+(x, 1)) ⇔ add'(0', _gen_nil':add'5(x))
The following defined symbols remain to be analysed:
high', quicksort'
They will be analysed ascendingly in the following order:
high' < quicksort'
Proved the following rewrite lemma:
high'(_gen_0':s'4(0), _gen_nil':add'5(_n6050)) → _gen_nil':add'5(0), rt ∈ Ω(1 + n6050)
Induction Base:
high'(_gen_0':s'4(0), _gen_nil':add'5(0)) →RΩ(1)
nil'
Induction Step:
high'(_gen_0':s'4(0), _gen_nil':add'5(+(_$n6051, 1))) →RΩ(1)
if_high'(le'(0', _gen_0':s'4(0)), _gen_0':s'4(0), add'(0', _gen_nil':add'5(_$n6051))) →LΩ(1)
if_high'(true', _gen_0':s'4(0), add'(0', _gen_nil':add'5(_$n6051))) →RΩ(1)
high'(_gen_0':s'4(0), _gen_nil':add'5(_$n6051)) →IH
_gen_nil':add'5(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, add'(m, x)) → if_low'(le'(m, n), n, add'(m, x))
if_low'(true', n, add'(m, x)) → add'(m, low'(n, x))
if_low'(false', n, add'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, add'(m, x)) → if_high'(le'(m, n), n, add'(m, x))
if_high'(true', n, add'(m, x)) → high'(n, x)
if_high'(false', n, add'(m, x)) → add'(m, high'(n, x))
head'(add'(n, x)) → n
tail'(add'(n, x)) → x
isempty'(nil') → true'
isempty'(add'(n, x)) → false'
quicksort'(x) → if_qs'(isempty'(x), low'(head'(x), tail'(x)), head'(x), high'(head'(x), tail'(x)))
if_qs'(true', x, n, y) → nil'
if_qs'(false', x, n, y) → app'(quicksort'(x), add'(n, quicksort'(y)))
Types:
le' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: 0':s' → nil':add' → nil':add'
low' :: 0':s' → nil':add' → nil':add'
if_low' :: true':false' → 0':s' → nil':add' → nil':add'
high' :: 0':s' → nil':add' → nil':add'
if_high' :: true':false' → 0':s' → nil':add' → nil':add'
head' :: nil':add' → 0':s'
tail' :: nil':add' → nil':add'
isempty' :: nil':add' → true':false'
quicksort' :: nil':add' → nil':add'
if_qs' :: true':false' → nil':add' → 0':s' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
le'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
app'(_gen_nil':add'5(_n1109), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n1109, b)), rt ∈ Ω(1 + n1109)
low'(_gen_0':s'4(0), _gen_nil':add'5(_n2747)) → _gen_nil':add'5(_n2747), rt ∈ Ω(1 + n2747)
high'(_gen_0':s'4(0), _gen_nil':add'5(_n6050)) → _gen_nil':add'5(0), rt ∈ Ω(1 + n6050)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':add'5(0) ⇔ nil'
_gen_nil':add'5(+(x, 1)) ⇔ add'(0', _gen_nil':add'5(x))
The following defined symbols remain to be analysed:
quicksort'
Proved the following rewrite lemma:
quicksort'(_gen_nil':add'5(_n9143)) → _gen_nil':add'5(_n9143), rt ∈ Ω(1 + n9143 + n91432)
Induction Base:
quicksort'(_gen_nil':add'5(0)) →RΩ(1)
if_qs'(isempty'(_gen_nil':add'5(0)), low'(head'(_gen_nil':add'5(0)), tail'(_gen_nil':add'5(0))), head'(_gen_nil':add'5(0)), high'(head'(_gen_nil':add'5(0)), tail'(_gen_nil':add'5(0)))) →RΩ(1)
if_qs'(true', low'(head'(_gen_nil':add'5(0)), tail'(_gen_nil':add'5(0))), head'(_gen_nil':add'5(0)), high'(head'(_gen_nil':add'5(0)), tail'(_gen_nil':add'5(0)))) →RΩ(1)
nil'
Induction Step:
quicksort'(_gen_nil':add'5(+(_$n9144, 1))) →RΩ(1)
if_qs'(isempty'(_gen_nil':add'5(+(_$n9144, 1))), low'(head'(_gen_nil':add'5(+(_$n9144, 1))), tail'(_gen_nil':add'5(+(_$n9144, 1)))), head'(_gen_nil':add'5(+(_$n9144, 1))), high'(head'(_gen_nil':add'5(+(_$n9144, 1))), tail'(_gen_nil':add'5(+(_$n9144, 1))))) →RΩ(1)
if_qs'(false', low'(head'(_gen_nil':add'5(+(1, _$n9144))), tail'(_gen_nil':add'5(+(1, _$n9144)))), head'(_gen_nil':add'5(+(1, _$n9144))), high'(head'(_gen_nil':add'5(+(1, _$n9144))), tail'(_gen_nil':add'5(+(1, _$n9144))))) →RΩ(1)
if_qs'(false', low'(0', tail'(_gen_nil':add'5(+(1, _$n9144)))), head'(_gen_nil':add'5(+(1, _$n9144))), high'(head'(_gen_nil':add'5(+(1, _$n9144))), tail'(_gen_nil':add'5(+(1, _$n9144))))) →RΩ(1)
if_qs'(false', low'(0', _gen_nil':add'5(_$n9144)), head'(_gen_nil':add'5(+(1, _$n9144))), high'(head'(_gen_nil':add'5(+(1, _$n9144))), tail'(_gen_nil':add'5(+(1, _$n9144))))) →LΩ(1 + $n9144)
if_qs'(false', _gen_nil':add'5(_$n9144), head'(_gen_nil':add'5(+(1, _$n9144))), high'(head'(_gen_nil':add'5(+(1, _$n9144))), tail'(_gen_nil':add'5(+(1, _$n9144))))) →RΩ(1)
if_qs'(false', _gen_nil':add'5(_$n9144), 0', high'(head'(_gen_nil':add'5(+(1, _$n9144))), tail'(_gen_nil':add'5(+(1, _$n9144))))) →RΩ(1)
if_qs'(false', _gen_nil':add'5(_$n9144), 0', high'(0', tail'(_gen_nil':add'5(+(1, _$n9144))))) →RΩ(1)
if_qs'(false', _gen_nil':add'5(_$n9144), 0', high'(0', _gen_nil':add'5(_$n9144))) →LΩ(1 + $n9144)
if_qs'(false', _gen_nil':add'5(_$n9144), 0', _gen_nil':add'5(0)) →RΩ(1)
app'(quicksort'(_gen_nil':add'5(_$n9144)), add'(0', quicksort'(_gen_nil':add'5(0)))) →IH
app'(_gen_nil':add'5(_$n9144), add'(0', quicksort'(_gen_nil':add'5(0)))) →RΩ(1)
app'(_gen_nil':add'5(_$n9144), add'(0', if_qs'(isempty'(_gen_nil':add'5(0)), low'(head'(_gen_nil':add'5(0)), tail'(_gen_nil':add'5(0))), head'(_gen_nil':add'5(0)), high'(head'(_gen_nil':add'5(0)), tail'(_gen_nil':add'5(0)))))) →RΩ(1)
app'(_gen_nil':add'5(_$n9144), add'(0', if_qs'(true', low'(head'(_gen_nil':add'5(0)), tail'(_gen_nil':add'5(0))), head'(_gen_nil':add'5(0)), high'(head'(_gen_nil':add'5(0)), tail'(_gen_nil':add'5(0)))))) →RΩ(1)
app'(_gen_nil':add'5(_$n9144), add'(0', nil')) →LΩ(1 + $n9144)
_gen_nil':add'5(+(_$n9144, +(0, 1)))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, add'(m, x)) → if_low'(le'(m, n), n, add'(m, x))
if_low'(true', n, add'(m, x)) → add'(m, low'(n, x))
if_low'(false', n, add'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, add'(m, x)) → if_high'(le'(m, n), n, add'(m, x))
if_high'(true', n, add'(m, x)) → high'(n, x)
if_high'(false', n, add'(m, x)) → add'(m, high'(n, x))
head'(add'(n, x)) → n
tail'(add'(n, x)) → x
isempty'(nil') → true'
isempty'(add'(n, x)) → false'
quicksort'(x) → if_qs'(isempty'(x), low'(head'(x), tail'(x)), head'(x), high'(head'(x), tail'(x)))
if_qs'(true', x, n, y) → nil'
if_qs'(false', x, n, y) → app'(quicksort'(x), add'(n, quicksort'(y)))
Types:
le' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: 0':s' → nil':add' → nil':add'
low' :: 0':s' → nil':add' → nil':add'
if_low' :: true':false' → 0':s' → nil':add' → nil':add'
high' :: 0':s' → nil':add' → nil':add'
if_high' :: true':false' → 0':s' → nil':add' → nil':add'
head' :: nil':add' → 0':s'
tail' :: nil':add' → nil':add'
isempty' :: nil':add' → true':false'
quicksort' :: nil':add' → nil':add'
if_qs' :: true':false' → nil':add' → 0':s' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
le'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
app'(_gen_nil':add'5(_n1109), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n1109, b)), rt ∈ Ω(1 + n1109)
low'(_gen_0':s'4(0), _gen_nil':add'5(_n2747)) → _gen_nil':add'5(_n2747), rt ∈ Ω(1 + n2747)
high'(_gen_0':s'4(0), _gen_nil':add'5(_n6050)) → _gen_nil':add'5(0), rt ∈ Ω(1 + n6050)
quicksort'(_gen_nil':add'5(_n9143)) → _gen_nil':add'5(_n9143), rt ∈ Ω(1 + n9143 + n91432)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':add'5(0) ⇔ nil'
_gen_nil':add'5(+(x, 1)) ⇔ add'(0', _gen_nil':add'5(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
quicksort'(_gen_nil':add'5(_n9143)) → _gen_nil':add'5(_n9143), rt ∈ Ω(1 + n9143 + n91432)