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

length(nil) → 0
length(cons(x, l)) → s(length(l))
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
tail(nil) → nil
tail(cons(x, l)) → l
reverse(l) → rev(0, l, nil, l)
rev(x, l, accu, orig) → if(lt(x, length(orig)), x, l, accu, orig)
if(true, x, l, accu, orig) → rev(s(x), tail(l), cons(head(l), accu), orig)
if(false, x, l, accu, orig) → accu

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu

Rewrite Strategy: INNERMOST

Infered types.

Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu

Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'

Heuristically decided to analyse the following defined symbols:
length', lt', rev'

They will be analysed ascendingly in the following order:
length' < rev'
lt' < rev'

Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu

Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'

Generator Equations:
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(undefined', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
length', lt', rev'

They will be analysed ascendingly in the following order:
length' < rev'
lt' < rev'

Proved the following rewrite lemma:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)

Induction Base:
length'(_gen_nil':cons'6(0)) →RΩ(1)
0'

Induction Step:
length'(_gen_nil':cons'6(+(_\$n9, 1))) →RΩ(1)
s'(length'(_gen_nil':cons'6(_\$n9))) →IH
s'(_gen_0':s'5(_\$n9))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu

Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)

Generator Equations:
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(undefined', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
lt', rev'

They will be analysed ascendingly in the following order:
lt' < rev'

Proved the following rewrite lemma:
lt'(_gen_0':s'5(_n520), _gen_0':s'5(_n520)) → false', rt ∈ Ω(1 + n520)

Induction Base:
lt'(_gen_0':s'5(0), _gen_0':s'5(0)) →RΩ(1)
false'

Induction Step:
lt'(_gen_0':s'5(+(_\$n521, 1)), _gen_0':s'5(+(_\$n521, 1))) →RΩ(1)
lt'(_gen_0':s'5(_\$n521), _gen_0':s'5(_\$n521)) →IH
false'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu

Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)
lt'(_gen_0':s'5(_n520), _gen_0':s'5(_n520)) → false', rt ∈ Ω(1 + n520)

Generator Equations:
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(undefined', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
rev'

Could not prove a rewrite lemma for the defined symbol rev'.

Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu

Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)
lt'(_gen_0':s'5(_n520), _gen_0':s'5(_n520)) → false', rt ∈ Ω(1 + n520)

Generator Equations:
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(undefined', _gen_nil':cons'6(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)