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

naiverev(Cons(x, xs)) → app(naiverev(xs), Cons(x, Nil))
app(Cons(x, xs), ys) → Cons(x, app(xs, ys))
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
naiverev(Nil) → Nil
app(Nil, ys) → ys
goal(xs) → naiverev(xs)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


naiverev'(Cons'(x, xs)) → app'(naiverev'(xs), Cons'(x, Nil'))
app'(Cons'(x, xs), ys) → Cons'(x, app'(xs, ys))
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
naiverev'(Nil') → Nil'
app'(Nil', ys) → ys
goal'(xs) → naiverev'(xs)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

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


naiverev'(Cons'(xs)) → app'(naiverev'(xs), Cons'(Nil'))
app'(Cons'(xs), ys) → Cons'(app'(xs, ys))
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
naiverev'(Nil') → Nil'
app'(Nil', ys) → ys
goal'(xs) → naiverev'(xs)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
naiverev'(Cons'(xs)) → app'(naiverev'(xs), Cons'(Nil'))
app'(Cons'(xs), ys) → Cons'(app'(xs, ys))
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
naiverev'(Nil') → Nil'
app'(Nil', ys) → ys
goal'(xs) → naiverev'(xs)

Types:
naiverev' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
app' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_True':False'2 :: True':False'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
naiverev', app'

They will be analysed ascendingly in the following order:
app' < naiverev'

Rules:
naiverev'(Cons'(xs)) → app'(naiverev'(xs), Cons'(Nil'))
app'(Cons'(xs), ys) → Cons'(app'(xs, ys))
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
naiverev'(Nil') → Nil'
app'(Nil', ys) → ys
goal'(xs) → naiverev'(xs)

Types:
naiverev' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
app' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_True':False'2 :: True':False'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Generator Equations:
_gen_Cons':Nil'3(0) ⇔ Nil'
_gen_Cons':Nil'3(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'3(x))

The following defined symbols remain to be analysed:
app', naiverev'

They will be analysed ascendingly in the following order:
app' < naiverev'

Proved the following rewrite lemma:
app'(_gen_Cons':Nil'3(_n5), _gen_Cons':Nil'3(b)) → _gen_Cons':Nil'3(+(_n5, b)), rt ∈ Ω(1 + n5)

Induction Base:
app'(_gen_Cons':Nil'3(0), _gen_Cons':Nil'3(b)) →RΩ(1)
_gen_Cons':Nil'3(b)

Induction Step:
app'(_gen_Cons':Nil'3(+(_$n6, 1)), _gen_Cons':Nil'3(_b140)) →RΩ(1)
Cons'(app'(_gen_Cons':Nil'3(_$n6), _gen_Cons':Nil'3(_b140))) →IH
Cons'(_gen_Cons':Nil'3(+(_$n6, _b140)))

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

Rules:
naiverev'(Cons'(xs)) → app'(naiverev'(xs), Cons'(Nil'))
app'(Cons'(xs), ys) → Cons'(app'(xs, ys))
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
naiverev'(Nil') → Nil'
app'(Nil', ys) → ys
goal'(xs) → naiverev'(xs)

Types:
naiverev' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
app' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_True':False'2 :: True':False'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Lemmas:
app'(_gen_Cons':Nil'3(_n5), _gen_Cons':Nil'3(b)) → _gen_Cons':Nil'3(+(_n5, b)), rt ∈ Ω(1 + n5)

Generator Equations:
_gen_Cons':Nil'3(0) ⇔ Nil'
_gen_Cons':Nil'3(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'3(x))

The following defined symbols remain to be analysed:
naiverev'

Proved the following rewrite lemma:
naiverev'(_gen_Cons':Nil'3(_n423)) → _gen_Cons':Nil'3(_n423), rt ∈ Ω(1 + n423 + n4232)

Induction Base:
naiverev'(_gen_Cons':Nil'3(0)) →RΩ(1)
Nil'

Induction Step:
naiverev'(_gen_Cons':Nil'3(+(_$n424, 1))) →RΩ(1)
app'(naiverev'(_gen_Cons':Nil'3(_$n424)), Cons'(Nil')) →IH
app'(_gen_Cons':Nil'3(_$n424), Cons'(Nil')) →LΩ(1 + $n424)
_gen_Cons':Nil'3(+(_$n424, +(0, 1)))

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

Rules:
naiverev'(Cons'(xs)) → app'(naiverev'(xs), Cons'(Nil'))
app'(Cons'(xs), ys) → Cons'(app'(xs, ys))
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
naiverev'(Nil') → Nil'
app'(Nil', ys) → ys
goal'(xs) → naiverev'(xs)

Types:
naiverev' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
app' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_True':False'2 :: True':False'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Lemmas:
app'(_gen_Cons':Nil'3(_n5), _gen_Cons':Nil'3(b)) → _gen_Cons':Nil'3(+(_n5, b)), rt ∈ Ω(1 + n5)
naiverev'(_gen_Cons':Nil'3(_n423)) → _gen_Cons':Nil'3(_n423), rt ∈ Ω(1 + n423 + n4232)

Generator Equations:
_gen_Cons':Nil'3(0) ⇔ Nil'
_gen_Cons':Nil'3(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
naiverev'(_gen_Cons':Nil'3(_n423)) → _gen_Cons':Nil'3(_n423), rt ∈ Ω(1 + n423 + n4232)