odd(S(x)) → even(x)
even(S(x)) → odd(x)
odd(0) → 0
even(0) → S(0)
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')
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)