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

list(Cons(x, xs)) → list(xs)
list(Nil) → True
list(Nil) → isEmpty[Match](Nil)
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
goal(x) → list(x)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


list'(Cons'(x, xs)) → list'(xs)
list'(Nil') → True'
list'(Nil') → isEmpty[Match]'(Nil')
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
goal'(x) → list'(x)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0
isEmpty[Match]'/0

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


list'(Cons'(xs)) → list'(xs)
list'(Nil') → True'
list'(Nil') → isEmpty[Match]'
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
goal'(x) → list'(x)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
list'(Cons'(xs)) → list'(xs)
list'(Nil') → True'
list'(Nil') → isEmpty[Match]'
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
goal'(x) → list'(x)

Types:
list' :: Cons':Nil' → True':isEmpty[Match]':False'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
True' :: True':isEmpty[Match]':False'
isEmpty[Match]' :: True':isEmpty[Match]':False'
notEmpty' :: Cons':Nil' → True':isEmpty[Match]':False'
False' :: True':isEmpty[Match]':False'
goal' :: Cons':Nil' → True':isEmpty[Match]':False'
_hole_True':isEmpty[Match]':False'1 :: True':isEmpty[Match]':False'
_hole_Cons':Nil'2 :: Cons':Nil'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
list'

Rules:
list'(Cons'(xs)) → list'(xs)
list'(Nil') → True'
list'(Nil') → isEmpty[Match]'
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
goal'(x) → list'(x)

Types:
list' :: Cons':Nil' → True':isEmpty[Match]':False'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
True' :: True':isEmpty[Match]':False'
isEmpty[Match]' :: True':isEmpty[Match]':False'
notEmpty' :: Cons':Nil' → True':isEmpty[Match]':False'
False' :: True':isEmpty[Match]':False'
goal' :: Cons':Nil' → True':isEmpty[Match]':False'
_hole_True':isEmpty[Match]':False'1 :: True':isEmpty[Match]':False'
_hole_Cons':Nil'2 :: Cons':Nil'
_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:
list'

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

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

Induction Step:
list'(_gen_Cons':Nil'3(+(_$n6, 1))) →RΩ(1)
list'(_gen_Cons':Nil'3(_$n6)) →IH
True'

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

Rules:
list'(Cons'(xs)) → list'(xs)
list'(Nil') → True'
list'(Nil') → isEmpty[Match]'
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
goal'(x) → list'(x)

Types:
list' :: Cons':Nil' → True':isEmpty[Match]':False'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
True' :: True':isEmpty[Match]':False'
isEmpty[Match]' :: True':isEmpty[Match]':False'
notEmpty' :: Cons':Nil' → True':isEmpty[Match]':False'
False' :: True':isEmpty[Match]':False'
goal' :: Cons':Nil' → True':isEmpty[Match]':False'
_hole_True':isEmpty[Match]':False'1 :: True':isEmpty[Match]':False'
_hole_Cons':Nil'2 :: Cons':Nil'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

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

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 Ω(n) was proven with the following lemma:
list'(_gen_Cons':Nil'3(_n5)) → True', rt ∈ Ω(1 + n5)