*** 1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(tail(X)) -> a__tail(mark(X)) mark(zeros()) -> a__zeros() Weak DP Rules: Weak TRS Rules: Signature: {a__tail/1,a__zeros/0,mark/1} / {0/0,cons/2,tail/1,zeros/0} Obligation: Innermost basic terms: {a__tail,a__zeros,mark}/{0,cons,tail,zeros} Applied Processor: Bounds {initialAutomaton = perSymbol, enrichment = match} Proof: The problem is match-bounded by 4. The enriched problem is compatible with follwoing automaton. 0_0() -> 1 0_1() -> 2 0_1() -> 5 0_1() -> 8 0_2() -> 10 0_4() -> 12 a__tail_0(1) -> 2 a__tail_0(4) -> 2 a__tail_0(6) -> 2 a__tail_0(7) -> 2 a__tail_1(2) -> 2 a__tail_1(2) -> 5 a__zeros_0() -> 3 a__zeros_1() -> 2 a__zeros_1() -> 5 a__zeros_3() -> 2 a__zeros_3() -> 5 cons_0(1,1) -> 4 cons_0(1,4) -> 4 cons_0(1,6) -> 4 cons_0(1,7) -> 4 cons_0(4,1) -> 4 cons_0(4,4) -> 4 cons_0(4,6) -> 4 cons_0(4,7) -> 4 cons_0(6,1) -> 4 cons_0(6,4) -> 4 cons_0(6,6) -> 4 cons_0(6,7) -> 4 cons_0(7,1) -> 4 cons_0(7,4) -> 4 cons_0(7,6) -> 4 cons_0(7,7) -> 4 cons_1(2,1) -> 2 cons_1(2,1) -> 5 cons_1(2,4) -> 2 cons_1(2,4) -> 5 cons_1(2,6) -> 2 cons_1(2,6) -> 5 cons_1(2,7) -> 2 cons_1(2,7) -> 5 cons_1(8,9) -> 3 cons_2(10,11) -> 2 cons_2(10,11) -> 5 cons_4(12,13) -> 2 cons_4(12,13) -> 5 mark_0(1) -> 5 mark_0(4) -> 5 mark_0(6) -> 5 mark_0(7) -> 5 mark_1(1) -> 2 mark_1(4) -> 2 mark_1(6) -> 2 mark_1(7) -> 2 mark_2(1) -> 2 mark_2(1) -> 5 mark_2(4) -> 2 mark_2(4) -> 5 mark_2(6) -> 2 mark_2(6) -> 5 mark_2(7) -> 2 mark_2(7) -> 5 mark_2(11) -> 2 mark_2(11) -> 5 mark_2(13) -> 2 mark_2(13) -> 5 tail_0(1) -> 6 tail_0(4) -> 6 tail_0(6) -> 6 tail_0(7) -> 6 tail_1(1) -> 2 tail_1(4) -> 2 tail_1(6) -> 2 tail_1(7) -> 2 tail_2(2) -> 2 tail_2(2) -> 5 zeros_0() -> 7 zeros_1() -> 3 zeros_1() -> 9 zeros_2() -> 2 zeros_2() -> 5 zeros_2() -> 11 zeros_4() -> 2 zeros_4() -> 5 zeros_4() -> 13 *** 1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(tail(X)) -> a__tail(mark(X)) mark(zeros()) -> a__zeros() Signature: {a__tail/1,a__zeros/0,mark/1} / {0/0,cons/2,tail/1,zeros/0} Obligation: Innermost basic terms: {a__tail,a__zeros,mark}/{0,cons,tail,zeros} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).