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

odd(Cons(x, xs)) → even(xs)
odd(Nil) → False
even(Cons(x, xs)) → odd(xs)
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
even(Nil) → True
evenodd(x) → even(x)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


odd'(Cons'(x, xs)) → even'(xs)
odd'(Nil') → False'
even'(Cons'(x, xs)) → odd'(xs)
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
even'(Nil') → True'
evenodd'(x) → even'(x)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

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


odd'(Cons'(xs)) → even'(xs)
odd'(Nil') → False'
even'(Cons'(xs)) → odd'(xs)
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
even'(Nil') → True'
evenodd'(x) → even'(x)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
odd'(Cons'(xs)) → even'(xs)
odd'(Nil') → False'
even'(Cons'(xs)) → odd'(xs)
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
even'(Nil') → True'
evenodd'(x) → even'(x)

Types:
odd' :: Cons':Nil' → False':True'
Cons' :: Cons':Nil' → Cons':Nil'
even' :: Cons':Nil' → False':True'
Nil' :: Cons':Nil'
False' :: False':True'
notEmpty' :: Cons':Nil' → False':True'
True' :: False':True'
evenodd' :: Cons':Nil' → False':True'
_hole_False':True'1 :: False':True'
_hole_Cons':Nil'2 :: Cons':Nil'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
odd', even'

They will be analysed ascendingly in the following order:
odd' = even'

Rules:
odd'(Cons'(xs)) → even'(xs)
odd'(Nil') → False'
even'(Cons'(xs)) → odd'(xs)
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
even'(Nil') → True'
evenodd'(x) → even'(x)

Types:
odd' :: Cons':Nil' → False':True'
Cons' :: Cons':Nil' → Cons':Nil'
even' :: Cons':Nil' → False':True'
Nil' :: Cons':Nil'
False' :: False':True'
notEmpty' :: Cons':Nil' → False':True'
True' :: False':True'
evenodd' :: Cons':Nil' → False':True'
_hole_False':True'1 :: False':True'
_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:
even', odd'

They will be analysed ascendingly in the following order:
odd' = even'

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

Induction Base:
even'(_gen_Cons':Nil'3(*(2, 0))) →RΩ(1)
True'

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

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

Rules:
odd'(Cons'(xs)) → even'(xs)
odd'(Nil') → False'
even'(Cons'(xs)) → odd'(xs)
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
even'(Nil') → True'
evenodd'(x) → even'(x)

Types:
odd' :: Cons':Nil' → False':True'
Cons' :: Cons':Nil' → Cons':Nil'
even' :: Cons':Nil' → False':True'
Nil' :: Cons':Nil'
False' :: False':True'
notEmpty' :: Cons':Nil' → False':True'
True' :: False':True'
evenodd' :: Cons':Nil' → False':True'
_hole_False':True'1 :: False':True'
_hole_Cons':Nil'2 :: Cons':Nil'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Lemmas:
even'(_gen_Cons':Nil'3(*(2, _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))

The following defined symbols remain to be analysed:
odd'

They will be analysed ascendingly in the following order:
odd' = even'

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

Rules:
odd'(Cons'(xs)) → even'(xs)
odd'(Nil') → False'
even'(Cons'(xs)) → odd'(xs)
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
even'(Nil') → True'
evenodd'(x) → even'(x)

Types:
odd' :: Cons':Nil' → False':True'
Cons' :: Cons':Nil' → Cons':Nil'
even' :: Cons':Nil' → False':True'
Nil' :: Cons':Nil'
False' :: False':True'
notEmpty' :: Cons':Nil' → False':True'
True' :: False':True'
evenodd' :: Cons':Nil' → False':True'
_hole_False':True'1 :: False':True'
_hole_Cons':Nil'2 :: Cons':Nil'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Lemmas:
even'(_gen_Cons':Nil'3(*(2, _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:
even'(_gen_Cons':Nil'3(*(2, _n5))) → True', rt ∈ Ω(1 + n5)