empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
empty'(nil') → true'
empty'(cons'(x, l)) → false'
head'(cons'(x, l)) → x
tail'(nil') → nil'
tail'(cons'(x, l)) → l
rev'(nil') → nil'
rev'(cons'(x, l)) → cons'(rev1'(x, l), rev2'(x, l))
last'(x, l) → if'(empty'(l), x, l)
if'(true', x, l) → x
if'(false', x, l) → last'(head'(l), tail'(l))
rev2'(x, nil') → nil'
rev2'(x, cons'(y, l)) → rev'(cons'(x, rev2'(y, l)))
Sliced the following arguments:
rev1'/0
rev1'/1
Runtime Complexity TRS:
The TRS R consists of the following rules:
empty'(nil') → true'
empty'(cons'(x, l)) → false'
head'(cons'(x, l)) → x
tail'(nil') → nil'
tail'(cons'(x, l)) → l
rev'(nil') → nil'
rev'(cons'(x, l)) → cons'(rev1', rev2'(x, l))
last'(x, l) → if'(empty'(l), x, l)
if'(true', x, l) → x
if'(false', x, l) → last'(head'(l), tail'(l))
rev2'(x, nil') → nil'
rev2'(x, cons'(y, l)) → rev'(cons'(x, rev2'(y, l)))
Infered types.
Rules:
empty'(nil') → true'
empty'(cons'(x, l)) → false'
head'(cons'(x, l)) → x
tail'(nil') → nil'
tail'(cons'(x, l)) → l
rev'(nil') → nil'
rev'(cons'(x, l)) → cons'(rev1', rev2'(x, l))
last'(x, l) → if'(empty'(l), x, l)
if'(true', x, l) → x
if'(false', x, l) → last'(head'(l), tail'(l))
rev2'(x, nil') → nil'
rev2'(x, cons'(y, l)) → rev'(cons'(x, rev2'(y, l)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: rev1' → nil':cons' → nil':cons'
false' :: true':false'
head' :: nil':cons' → rev1'
tail' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons'
rev1' :: rev1'
rev2' :: rev1' → nil':cons' → nil':cons'
last' :: rev1' → nil':cons' → rev1'
if' :: true':false' → rev1' → nil':cons' → rev1'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_rev1'3 :: rev1'
_gen_nil':cons'4 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
rev', rev2', last'
They will be analysed ascendingly in the following order:
rev' = rev2'
Rules:
empty'(nil') → true'
empty'(cons'(x, l)) → false'
head'(cons'(x, l)) → x
tail'(nil') → nil'
tail'(cons'(x, l)) → l
rev'(nil') → nil'
rev'(cons'(x, l)) → cons'(rev1', rev2'(x, l))
last'(x, l) → if'(empty'(l), x, l)
if'(true', x, l) → x
if'(false', x, l) → last'(head'(l), tail'(l))
rev2'(x, nil') → nil'
rev2'(x, cons'(y, l)) → rev'(cons'(x, rev2'(y, l)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: rev1' → nil':cons' → nil':cons'
false' :: true':false'
head' :: nil':cons' → rev1'
tail' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons'
rev1' :: rev1'
rev2' :: rev1' → nil':cons' → nil':cons'
last' :: rev1' → nil':cons' → rev1'
if' :: true':false' → rev1' → nil':cons' → rev1'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_rev1'3 :: rev1'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(rev1', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
last', rev', rev2'
They will be analysed ascendingly in the following order:
rev' = rev2'
Proved the following rewrite lemma:
last'(rev1', _gen_nil':cons'4(_n6)) → rev1', rt ∈ Ω(1 + n6)
Induction Base:
last'(rev1', _gen_nil':cons'4(0)) →RΩ(1)
if'(empty'(_gen_nil':cons'4(0)), rev1', _gen_nil':cons'4(0)) →RΩ(1)
if'(true', rev1', _gen_nil':cons'4(0)) →RΩ(1)
rev1'
Induction Step:
last'(rev1', _gen_nil':cons'4(+(_$n7, 1))) →RΩ(1)
if'(empty'(_gen_nil':cons'4(+(_$n7, 1))), rev1', _gen_nil':cons'4(+(_$n7, 1))) →RΩ(1)
if'(false', rev1', _gen_nil':cons'4(+(1, _$n7))) →RΩ(1)
last'(head'(_gen_nil':cons'4(+(1, _$n7))), tail'(_gen_nil':cons'4(+(1, _$n7)))) →RΩ(1)
last'(rev1', tail'(_gen_nil':cons'4(+(1, _$n7)))) →RΩ(1)
last'(rev1', _gen_nil':cons'4(_$n7)) →IH
rev1'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
empty'(nil') → true'
empty'(cons'(x, l)) → false'
head'(cons'(x, l)) → x
tail'(nil') → nil'
tail'(cons'(x, l)) → l
rev'(nil') → nil'
rev'(cons'(x, l)) → cons'(rev1', rev2'(x, l))
last'(x, l) → if'(empty'(l), x, l)
if'(true', x, l) → x
if'(false', x, l) → last'(head'(l), tail'(l))
rev2'(x, nil') → nil'
rev2'(x, cons'(y, l)) → rev'(cons'(x, rev2'(y, l)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: rev1' → nil':cons' → nil':cons'
false' :: true':false'
head' :: nil':cons' → rev1'
tail' :: nil':cons' → nil':cons'
rev' :: nil':cons' → nil':cons'
rev1' :: rev1'
rev2' :: rev1' → nil':cons' → nil':cons'
last' :: rev1' → nil':cons' → rev1'
if' :: true':false' → rev1' → nil':cons' → rev1'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_rev1'3 :: rev1'
_gen_nil':cons'4 :: Nat → nil':cons'
Lemmas:
last'(rev1', _gen_nil':cons'4(_n6)) → rev1', rt ∈ Ω(1 + n6)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(rev1', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
rev2', rev'
They will be analysed ascendingly in the following order:
rev' = rev2'
Proved the following rewrite lemma:
rev2'(rev1', _gen_nil':cons'4(_n1218)) → _gen_nil':cons'4(_n1218), rt ∈ Ω(2n)
Induction Base:
rev2'(rev1', _gen_nil':cons'4(0)) →RΩ(1)
nil'
Induction Step:
rev2'(rev1', _gen_nil':cons'4(+(_$n1219, 1))) →RΩ(1)
rev'(cons'(rev1', rev2'(rev1', _gen_nil':cons'4(_$n1219)))) →IH
rev'(cons'(rev1', _gen_nil':cons'4(_$n1219))) →RΩ(1)
cons'(rev1', rev2'(rev1', _gen_nil':cons'4(_$n1219))) →IH
cons'(rev1', _gen_nil':cons'4(_$n1219))
We have rt ∈ Ω(2n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(2n)