*** 1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: anchored(Cons(x,xs),y) -> anchored(xs,Cons(Cons(Nil(),Nil()),y)) anchored(Nil(),y) -> y goal(x,y) -> anchored(x,y) Weak DP Rules: Weak TRS Rules: Signature: {anchored/2,goal/2} / {Cons/2,Nil/0} Obligation: Innermost basic terms: {anchored,goal}/{Cons,Nil} Applied Processor: Bounds {initialAutomaton = perSymbol, enrichment = match} Proof: The problem is match-bounded by 1. The enriched problem is compatible with follwoing automaton. Cons_0(1,1) -> 1 Cons_0(1,1) -> 3 Cons_0(1,1) -> 4 Cons_0(1,2) -> 1 Cons_0(1,2) -> 3 Cons_0(1,2) -> 4 Cons_0(2,1) -> 1 Cons_0(2,1) -> 3 Cons_0(2,1) -> 4 Cons_0(2,2) -> 1 Cons_0(2,2) -> 3 Cons_0(2,2) -> 4 Cons_1(6,1) -> 3 Cons_1(6,1) -> 4 Cons_1(6,1) -> 5 Cons_1(6,2) -> 3 Cons_1(6,2) -> 4 Cons_1(6,2) -> 5 Cons_1(6,5) -> 3 Cons_1(6,5) -> 4 Cons_1(6,5) -> 5 Cons_1(7,8) -> 6 Nil_0() -> 2 Nil_0() -> 3 Nil_0() -> 4 Nil_1() -> 7 Nil_1() -> 8 anchored_0(1,1) -> 3 anchored_0(1,2) -> 3 anchored_0(2,1) -> 3 anchored_0(2,2) -> 3 anchored_1(1,1) -> 4 anchored_1(1,2) -> 4 anchored_1(1,5) -> 3 anchored_1(1,5) -> 4 anchored_1(2,1) -> 4 anchored_1(2,2) -> 4 anchored_1(2,5) -> 3 anchored_1(2,5) -> 4 goal_0(1,1) -> 4 goal_0(1,2) -> 4 goal_0(2,1) -> 4 goal_0(2,2) -> 4 1 -> 3 1 -> 4 2 -> 3 2 -> 4 5 -> 3 5 -> 4 *** 1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: anchored(Cons(x,xs),y) -> anchored(xs,Cons(Cons(Nil(),Nil()),y)) anchored(Nil(),y) -> y goal(x,y) -> anchored(x,y) Signature: {anchored/2,goal/2} / {Cons/2,Nil/0} Obligation: Innermost basic terms: {anchored,goal}/{Cons,Nil} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).