*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
even(Cons(x,xs)) -> odd(xs)
even(Nil()) -> True()
evenodd(x) -> even(x)
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
odd(Cons(x,xs)) -> even(xs)
odd(Nil()) -> False()
Weak DP Rules:
Weak TRS Rules:
Signature:
{even/1,evenodd/1,notEmpty/1,odd/1} / {Cons/2,False/0,Nil/0,True/0}
Obligation:
Innermost
basic terms: {even,evenodd,notEmpty,odd}/{Cons,False,Nil,True}
Applied Processor:
Bounds {initialAutomaton = minimal, enrichment = match}
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with follwoing automaton.
Cons_0(2,2) -> 2
False_0() -> 2
False_1() -> 1
Nil_0() -> 2
True_0() -> 2
True_1() -> 1
even_0(2) -> 1
even_1(2) -> 1
evenodd_0(2) -> 1
notEmpty_0(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(Cons(x,xs)) -> odd(xs)
even(Nil()) -> True()
evenodd(x) -> even(x)
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
odd(Cons(x,xs)) -> even(xs)
odd(Nil()) -> False()
Signature:
{even/1,evenodd/1,notEmpty/1,odd/1} / {Cons/2,False/0,Nil/0,True/0}
Obligation:
Innermost
basic terms: {even,evenodd,notEmpty,odd}/{Cons,False,Nil,True}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).