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

odd(S(x)) → even(x)
even(S(x)) → odd(x)
odd(0) → 0
even(0) → S(0)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

odd'(S'(x)) → even'(x)
even'(S'(x)) → odd'(x)
odd'(0') → 0'
even'(0') → S'(0')

Rewrite Strategy: INNERMOST

Infered types.

Rules:
odd'(S'(x)) → even'(x)
even'(S'(x)) → odd'(x)
odd'(0') → 0'
even'(0') → S'(0')

Types:
odd' :: S':0' → S':0'
S' :: S':0' → S':0'
even' :: S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

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

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

Rules:
odd'(S'(x)) → even'(x)
even'(S'(x)) → odd'(x)
odd'(0') → 0'
even'(0') → S'(0')

Types:
odd' :: S':0' → S':0'
S' :: S':0' → S':0'
even' :: S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

Generator Equations:
_gen_S':0'2(0) ⇔ 0'
_gen_S':0'2(+(x, 1)) ⇔ S'(_gen_S':0'2(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_S':0'2(*(2, _n4))) → _gen_S':0'2(1), rt ∈ Ω(1 + n4)

Induction Base:
even'(_gen_S':0'2(*(2, 0))) →RΩ(1)
S'(0')

Induction Step:
even'(_gen_S':0'2(*(2, +(_\$n5, 1)))) →RΩ(1)
odd'(_gen_S':0'2(+(1, *(2, _\$n5)))) →RΩ(1)
even'(_gen_S':0'2(*(2, _\$n5))) →IH
_gen_S':0'2(1)

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

Rules:
odd'(S'(x)) → even'(x)
even'(S'(x)) → odd'(x)
odd'(0') → 0'
even'(0') → S'(0')

Types:
odd' :: S':0' → S':0'
S' :: S':0' → S':0'
even' :: S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

Lemmas:
even'(_gen_S':0'2(*(2, _n4))) → _gen_S':0'2(1), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_S':0'2(0) ⇔ 0'
_gen_S':0'2(+(x, 1)) ⇔ S'(_gen_S':0'2(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'(S'(x)) → even'(x)
even'(S'(x)) → odd'(x)
odd'(0') → 0'
even'(0') → S'(0')

Types:
odd' :: S':0' → S':0'
S' :: S':0' → S':0'
even' :: S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

Lemmas:
even'(_gen_S':0'2(*(2, _n4))) → _gen_S':0'2(1), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_S':0'2(0) ⇔ 0'
_gen_S':0'2(+(x, 1)) ⇔ S'(_gen_S':0'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
even'(_gen_S':0'2(*(2, _n4))) → _gen_S':0'2(1), rt ∈ Ω(1 + n4)