*** 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).