minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
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))
quicksort(nil) → nil
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Infered types.
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_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:
minus', quot', le', app', low', high', quicksort'
They will be analysed ascendingly in the following order:
minus' < quot'
le' < low'
le' < high'
app' < quicksort'
low' < quicksort'
high' < quicksort'
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_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:
minus', quot', le', app', low', high', quicksort'
They will be analysed ascendingly in the following order:
minus' < quot'
le' < low'
le' < high'
app' < quicksort'
low' < quicksort'
high' < quicksort'
Proved the following rewrite lemma:
minus'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
Induction Base:
minus'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
_gen_0':s'4(0)
Induction Step:
minus'(_gen_0':s'4(+(_$n8, 1)), _gen_0':s'4(+(_$n8, 1))) →RΩ(1)
minus'(_gen_0':s'4(_$n8), _gen_0':s'4(_$n8)) →IH
_gen_0':s'4(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
minus'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → _gen_0':s'4(0), 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:
quot', le', app', low', high', quicksort'
They will be analysed ascendingly in the following order:
le' < low'
le' < high'
app' < quicksort'
low' < quicksort'
high' < quicksort'
Could not prove a rewrite lemma for the defined symbol quot'.
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
minus'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → _gen_0':s'4(0), 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:
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(_n1396), _gen_0':s'4(_n1396)) → true', rt ∈ Ω(1 + n1396)
Induction Base:
le'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
true'
Induction Step:
le'(_gen_0':s'4(+(_$n1397, 1)), _gen_0':s'4(+(_$n1397, 1))) →RΩ(1)
le'(_gen_0':s'4(_$n1397), _gen_0':s'4(_$n1397)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
minus'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1396), _gen_0':s'4(_n1396)) → true', rt ∈ Ω(1 + n1396)
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(_n2432), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n2432, b)), rt ∈ Ω(1 + n2432)
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(+(_$n2433, 1)), _gen_nil':add'5(_b2663)) →RΩ(1)
add'(0', app'(_gen_nil':add'5(_$n2433), _gen_nil':add'5(_b2663))) →IH
add'(0', _gen_nil':add'5(+(_$n2433, _b2663)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
minus'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1396), _gen_0':s'4(_n1396)) → true', rt ∈ Ω(1 + n1396)
app'(_gen_nil':add'5(_n2432), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n2432, b)), rt ∈ Ω(1 + n2432)
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(_n3958)) → _gen_nil':add'5(_n3958), rt ∈ Ω(1 + n3958)
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(+(_$n3959, 1))) →RΩ(1)
if_low'(le'(0', _gen_0':s'4(0)), _gen_0':s'4(0), add'(0', _gen_nil':add'5(_$n3959))) →LΩ(1)
if_low'(true', _gen_0':s'4(0), add'(0', _gen_nil':add'5(_$n3959))) →RΩ(1)
add'(0', low'(_gen_0':s'4(0), _gen_nil':add'5(_$n3959))) →IH
add'(0', _gen_nil':add'5(_$n3959))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
minus'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1396), _gen_0':s'4(_n1396)) → true', rt ∈ Ω(1 + n1396)
app'(_gen_nil':add'5(_n2432), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n2432, b)), rt ∈ Ω(1 + n2432)
low'(_gen_0':s'4(0), _gen_nil':add'5(_n3958)) → _gen_nil':add'5(_n3958), rt ∈ Ω(1 + n3958)
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(_n7031)) → _gen_nil':add'5(0), rt ∈ Ω(1 + n7031)
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(+(_$n7032, 1))) →RΩ(1)
if_high'(le'(0', _gen_0':s'4(0)), _gen_0':s'4(0), add'(0', _gen_nil':add'5(_$n7032))) →LΩ(1)
if_high'(true', _gen_0':s'4(0), add'(0', _gen_nil':add'5(_$n7032))) →RΩ(1)
high'(_gen_0':s'4(0), _gen_nil':add'5(_$n7032)) →IH
_gen_nil':add'5(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
minus'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1396), _gen_0':s'4(_n1396)) → true', rt ∈ Ω(1 + n1396)
app'(_gen_nil':add'5(_n2432), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n2432, b)), rt ∈ Ω(1 + n2432)
low'(_gen_0':s'4(0), _gen_nil':add'5(_n3958)) → _gen_nil':add'5(_n3958), rt ∈ Ω(1 + n3958)
high'(_gen_0':s'4(0), _gen_nil':add'5(_n7031)) → _gen_nil':add'5(0), rt ∈ Ω(1 + n7031)
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(_n9918)) → _gen_nil':add'5(_n9918), rt ∈ Ω(1 + n9918 + n99182)
Induction Base:
quicksort'(_gen_nil':add'5(0)) →RΩ(1)
nil'
Induction Step:
quicksort'(_gen_nil':add'5(+(_$n9919, 1))) →RΩ(1)
app'(quicksort'(low'(0', _gen_nil':add'5(_$n9919))), add'(0', quicksort'(high'(0', _gen_nil':add'5(_$n9919))))) →LΩ(1 + $n9919)
app'(quicksort'(_gen_nil':add'5(_$n9919)), add'(0', quicksort'(high'(0', _gen_nil':add'5(_$n9919))))) →IH
app'(_gen_nil':add'5(_$n9919), add'(0', quicksort'(high'(0', _gen_nil':add'5(_$n9919))))) →LΩ(1 + $n9919)
app'(_gen_nil':add'5(_$n9919), add'(0', quicksort'(_gen_nil':add'5(0)))) →RΩ(1)
app'(_gen_nil':add'5(_$n9919), add'(0', nil')) →LΩ(1 + $n9919)
_gen_nil':add'5(+(_$n9919, +(0, 1)))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
minus'(x, 0') → x
minus'(s'(x), s'(y)) → minus'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(minus'(x, y), s'(y)))
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))
quicksort'(nil') → nil'
quicksort'(add'(n, x)) → app'(quicksort'(low'(n, x)), add'(n, quicksort'(high'(n, x))))
Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
le' :: 0':s' → 0':s' → true':false'
true' :: true':false'
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'
quicksort' :: nil':add' → nil':add'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_nil':add'3 :: nil':add'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':add'5 :: Nat → nil':add'
Lemmas:
minus'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
le'(_gen_0':s'4(_n1396), _gen_0':s'4(_n1396)) → true', rt ∈ Ω(1 + n1396)
app'(_gen_nil':add'5(_n2432), _gen_nil':add'5(b)) → _gen_nil':add'5(+(_n2432, b)), rt ∈ Ω(1 + n2432)
low'(_gen_0':s'4(0), _gen_nil':add'5(_n3958)) → _gen_nil':add'5(_n3958), rt ∈ Ω(1 + n3958)
high'(_gen_0':s'4(0), _gen_nil':add'5(_n7031)) → _gen_nil':add'5(0), rt ∈ Ω(1 + n7031)
quicksort'(_gen_nil':add'5(_n9918)) → _gen_nil':add'5(_n9918), rt ∈ Ω(1 + n9918 + n99182)
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(_n9918)) → _gen_nil':add'5(_n9918), rt ∈ Ω(1 + n9918 + n99182)