*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
even(0()) -> S(0())
even(S(x)) -> odd(x)
odd(0()) -> 0()
odd(S(x)) -> even(x)
Weak DP Rules:
Weak TRS Rules:
Signature:
{even/1,odd/1} / {0/0,S/1}
Obligation:
Innermost
basic terms: {even,odd}/{0,S}
Applied Processor:
Bounds {initialAutomaton = minimal, enrichment = match}
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with follwoing automaton.
0_0() -> 2
0_1() -> 1
0_1() -> 3
S_0(2) -> 2
S_1(3) -> 1
even_0(2) -> 1
even_1(2) -> 1
odd_0(2) -> 1
odd_1(2) -> 1
*** 1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
even(0()) -> S(0())
even(S(x)) -> odd(x)
odd(0()) -> 0()
odd(S(x)) -> even(x)
Signature:
{even/1,odd/1} / {0/0,S/1}
Obligation:
Innermost
basic terms: {even,odd}/{0,S}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).