isEmpty(nil) → true
isEmpty(cons(x, xs)) → false
last(cons(x, nil)) → x
last(cons(x, cons(y, ys))) → last(cons(y, ys))
dropLast(nil) → nil
dropLast(cons(x, nil)) → nil
dropLast(cons(x, cons(y, ys))) → cons(x, dropLast(cons(y, ys)))
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
reverse(xs) → rev(xs, nil)
rev(xs, ys) → if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
if(true, xs, ys, zs) → zs
if(false, xs, ys, zs) → rev(xs, ys)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
isEmpty'(nil') → true'
isEmpty'(cons'(x, xs)) → false'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, ys))) → last'(cons'(y, ys))
dropLast'(nil') → nil'
dropLast'(cons'(x, nil')) → nil'
dropLast'(cons'(x, cons'(y, ys))) → cons'(x, dropLast'(cons'(y, ys)))
append'(nil', ys) → ys
append'(cons'(x, xs), ys) → cons'(x, append'(xs, ys))
reverse'(xs) → rev'(xs, nil')
rev'(xs, ys) → if'(isEmpty'(xs), dropLast'(xs), append'(ys, last'(xs)), ys)
if'(true', xs, ys, zs) → zs
if'(false', xs, ys, zs) → rev'(xs, ys)
Infered types.
Rules:
isEmpty'(nil') → true'
isEmpty'(cons'(x, xs)) → false'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, ys))) → last'(cons'(y, ys))
dropLast'(nil') → nil'
dropLast'(cons'(x, nil')) → nil'
dropLast'(cons'(x, cons'(y, ys))) → cons'(x, dropLast'(cons'(y, ys)))
append'(nil', ys) → ys
append'(cons'(x, xs), ys) → cons'(x, append'(xs, ys))
reverse'(xs) → rev'(xs, nil')
rev'(xs, ys) → if'(isEmpty'(xs), dropLast'(xs), append'(ys, last'(xs)), ys)
if'(true', xs, ys, zs) → zs
if'(false', xs, ys, zs) → rev'(xs, ys)
Types:
isEmpty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: nil':cons' → nil':cons' → nil':cons'
false' :: true':false'
last' :: nil':cons' → nil':cons'
dropLast' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons' → nil':cons'
if' :: true':false' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_gen_nil':cons'3 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
last', dropLast', append', rev'
They will be analysed ascendingly in the following order:
last' < rev'
dropLast' < rev'
append' < rev'
Rules:
isEmpty'(nil') → true'
isEmpty'(cons'(x, xs)) → false'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, ys))) → last'(cons'(y, ys))
dropLast'(nil') → nil'
dropLast'(cons'(x, nil')) → nil'
dropLast'(cons'(x, cons'(y, ys))) → cons'(x, dropLast'(cons'(y, ys)))
append'(nil', ys) → ys
append'(cons'(x, xs), ys) → cons'(x, append'(xs, ys))
reverse'(xs) → rev'(xs, nil')
rev'(xs, ys) → if'(isEmpty'(xs), dropLast'(xs), append'(ys, last'(xs)), ys)
if'(true', xs, ys, zs) → zs
if'(false', xs, ys, zs) → rev'(xs, ys)
Types:
isEmpty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: nil':cons' → nil':cons' → nil':cons'
false' :: true':false'
last' :: nil':cons' → nil':cons'
dropLast' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons' → nil':cons'
if' :: true':false' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_gen_nil':cons'3 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
The following defined symbols remain to be analysed:
last', dropLast', append', rev'
They will be analysed ascendingly in the following order:
last' < rev'
dropLast' < rev'
append' < rev'
Proved the following rewrite lemma:
last'(_gen_nil':cons'3(+(1, _n5))) → _gen_nil':cons'3(0), rt ∈ Ω(1 + n5)
Induction Base:
last'(_gen_nil':cons'3(+(1, 0))) →RΩ(1)
nil'
Induction Step:
last'(_gen_nil':cons'3(+(1, +(_$n6, 1)))) →RΩ(1)
last'(cons'(nil', _gen_nil':cons'3(_$n6))) →IH
_gen_nil':cons'3(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
isEmpty'(nil') → true'
isEmpty'(cons'(x, xs)) → false'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, ys))) → last'(cons'(y, ys))
dropLast'(nil') → nil'
dropLast'(cons'(x, nil')) → nil'
dropLast'(cons'(x, cons'(y, ys))) → cons'(x, dropLast'(cons'(y, ys)))
append'(nil', ys) → ys
append'(cons'(x, xs), ys) → cons'(x, append'(xs, ys))
reverse'(xs) → rev'(xs, nil')
rev'(xs, ys) → if'(isEmpty'(xs), dropLast'(xs), append'(ys, last'(xs)), ys)
if'(true', xs, ys, zs) → zs
if'(false', xs, ys, zs) → rev'(xs, ys)
Types:
isEmpty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: nil':cons' → nil':cons' → nil':cons'
false' :: true':false'
last' :: nil':cons' → nil':cons'
dropLast' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons' → nil':cons'
if' :: true':false' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_gen_nil':cons'3 :: Nat → nil':cons'
Lemmas:
last'(_gen_nil':cons'3(+(1, _n5))) → _gen_nil':cons'3(0), rt ∈ Ω(1 + n5)
Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
The following defined symbols remain to be analysed:
dropLast', append', rev'
They will be analysed ascendingly in the following order:
dropLast' < rev'
append' < rev'
Proved the following rewrite lemma:
dropLast'(_gen_nil':cons'3(+(1, _n651))) → _gen_nil':cons'3(_n651), rt ∈ Ω(1 + n651)
Induction Base:
dropLast'(_gen_nil':cons'3(+(1, 0))) →RΩ(1)
nil'
Induction Step:
dropLast'(_gen_nil':cons'3(+(1, +(_$n652, 1)))) →RΩ(1)
cons'(nil', dropLast'(cons'(nil', _gen_nil':cons'3(_$n652)))) →IH
cons'(nil', _gen_nil':cons'3(_$n652))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
isEmpty'(nil') → true'
isEmpty'(cons'(x, xs)) → false'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, ys))) → last'(cons'(y, ys))
dropLast'(nil') → nil'
dropLast'(cons'(x, nil')) → nil'
dropLast'(cons'(x, cons'(y, ys))) → cons'(x, dropLast'(cons'(y, ys)))
append'(nil', ys) → ys
append'(cons'(x, xs), ys) → cons'(x, append'(xs, ys))
reverse'(xs) → rev'(xs, nil')
rev'(xs, ys) → if'(isEmpty'(xs), dropLast'(xs), append'(ys, last'(xs)), ys)
if'(true', xs, ys, zs) → zs
if'(false', xs, ys, zs) → rev'(xs, ys)
Types:
isEmpty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: nil':cons' → nil':cons' → nil':cons'
false' :: true':false'
last' :: nil':cons' → nil':cons'
dropLast' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons' → nil':cons'
if' :: true':false' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_gen_nil':cons'3 :: Nat → nil':cons'
Lemmas:
last'(_gen_nil':cons'3(+(1, _n5))) → _gen_nil':cons'3(0), rt ∈ Ω(1 + n5)
dropLast'(_gen_nil':cons'3(+(1, _n651))) → _gen_nil':cons'3(_n651), rt ∈ Ω(1 + n651)
Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
The following defined symbols remain to be analysed:
append', rev'
They will be analysed ascendingly in the following order:
append' < rev'
Proved the following rewrite lemma:
append'(_gen_nil':cons'3(_n1452), _gen_nil':cons'3(b)) → _gen_nil':cons'3(+(_n1452, b)), rt ∈ Ω(1 + n1452)
Induction Base:
append'(_gen_nil':cons'3(0), _gen_nil':cons'3(b)) →RΩ(1)
_gen_nil':cons'3(b)
Induction Step:
append'(_gen_nil':cons'3(+(_$n1453, 1)), _gen_nil':cons'3(_b1593)) →RΩ(1)
cons'(nil', append'(_gen_nil':cons'3(_$n1453), _gen_nil':cons'3(_b1593))) →IH
cons'(nil', _gen_nil':cons'3(+(_$n1453, _b1593)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
isEmpty'(nil') → true'
isEmpty'(cons'(x, xs)) → false'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, ys))) → last'(cons'(y, ys))
dropLast'(nil') → nil'
dropLast'(cons'(x, nil')) → nil'
dropLast'(cons'(x, cons'(y, ys))) → cons'(x, dropLast'(cons'(y, ys)))
append'(nil', ys) → ys
append'(cons'(x, xs), ys) → cons'(x, append'(xs, ys))
reverse'(xs) → rev'(xs, nil')
rev'(xs, ys) → if'(isEmpty'(xs), dropLast'(xs), append'(ys, last'(xs)), ys)
if'(true', xs, ys, zs) → zs
if'(false', xs, ys, zs) → rev'(xs, ys)
Types:
isEmpty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: nil':cons' → nil':cons' → nil':cons'
false' :: true':false'
last' :: nil':cons' → nil':cons'
dropLast' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons' → nil':cons'
if' :: true':false' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_gen_nil':cons'3 :: Nat → nil':cons'
Lemmas:
last'(_gen_nil':cons'3(+(1, _n5))) → _gen_nil':cons'3(0), rt ∈ Ω(1 + n5)
dropLast'(_gen_nil':cons'3(+(1, _n651))) → _gen_nil':cons'3(_n651), rt ∈ Ω(1 + n651)
append'(_gen_nil':cons'3(_n1452), _gen_nil':cons'3(b)) → _gen_nil':cons'3(+(_n1452, b)), rt ∈ Ω(1 + n1452)
Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
The following defined symbols remain to be analysed:
rev'
Could not prove a rewrite lemma for the defined symbol rev'.
Rules:
isEmpty'(nil') → true'
isEmpty'(cons'(x, xs)) → false'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, ys))) → last'(cons'(y, ys))
dropLast'(nil') → nil'
dropLast'(cons'(x, nil')) → nil'
dropLast'(cons'(x, cons'(y, ys))) → cons'(x, dropLast'(cons'(y, ys)))
append'(nil', ys) → ys
append'(cons'(x, xs), ys) → cons'(x, append'(xs, ys))
reverse'(xs) → rev'(xs, nil')
rev'(xs, ys) → if'(isEmpty'(xs), dropLast'(xs), append'(ys, last'(xs)), ys)
if'(true', xs, ys, zs) → zs
if'(false', xs, ys, zs) → rev'(xs, ys)
Types:
isEmpty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: nil':cons' → nil':cons' → nil':cons'
false' :: true':false'
last' :: nil':cons' → nil':cons'
dropLast' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons' → nil':cons'
if' :: true':false' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_gen_nil':cons'3 :: Nat → nil':cons'
Lemmas:
last'(_gen_nil':cons'3(+(1, _n5))) → _gen_nil':cons'3(0), rt ∈ Ω(1 + n5)
dropLast'(_gen_nil':cons'3(+(1, _n651))) → _gen_nil':cons'3(_n651), rt ∈ Ω(1 + n651)
append'(_gen_nil':cons'3(_n1452), _gen_nil':cons'3(b)) → _gen_nil':cons'3(+(_n1452, b)), rt ∈ Ω(1 + n1452)
Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
last'(_gen_nil':cons'3(+(1, _n5))) → _gen_nil':cons'3(0), rt ∈ Ω(1 + n5)