Runtime Complexity TRS:
The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, l)) → false
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)))

Rewrite Strategy: INNERMOST

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'
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)))

Rewrite Strategy: INNERMOST

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'
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)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
empty'(nil') → true'
empty'(cons'(x, l)) → false'
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'
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'
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'
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'(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'
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'
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)