*** 1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: eqZList(C(x1,x2),C(y1,y2)) -> and(eqZList(x1,y1),eqZList(x2,y2)) eqZList(C(x1,x2),Z()) -> False() eqZList(Z(),C(y1,y2)) -> False() eqZList(Z(),Z()) -> True() f(C(x1,x2)) -> C(f(x1),f(x2)) f(Z()) -> Z() first(C(x1,x2)) -> x1 g(x) -> x second(C(x1,x2)) -> x2 Weak DP Rules: Weak TRS Rules: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() Signature: {and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0,Z/0} Obligation: Innermost basic terms: {and,eqZList,f,first,g,second}/{C,False,True,Z} Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} Proof: The problem is match-bounded by 1. The enriched problem is compatible with follwoing automaton. C_0(2,2) -> 1 C_0(2,2) -> 2 C_1(5,6) -> 1 C_1(6,6) -> 5 C_1(6,6) -> 6 False_0() -> 1 False_0() -> 2 False_1() -> 1 False_1() -> 3 False_1() -> 4 True_0() -> 1 True_0() -> 2 True_1() -> 1 True_1() -> 3 True_1() -> 4 Z_0() -> 1 Z_0() -> 2 Z_1() -> 1 Z_1() -> 5 Z_1() -> 6 and_0(2,2) -> 1 and_1(3,4) -> 1 and_1(4,4) -> 3 and_1(4,4) -> 4 eqZList_0(2,2) -> 1 eqZList_1(2,2) -> 3 eqZList_1(2,2) -> 4 f_0(2) -> 1 f_1(2) -> 5 f_1(2) -> 6 first_0(2) -> 1 g_0(2) -> 1 second_0(2) -> 1 2 -> 1 *** 1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqZList(C(x1,x2),C(y1,y2)) -> and(eqZList(x1,y1),eqZList(x2,y2)) eqZList(C(x1,x2),Z()) -> False() eqZList(Z(),C(y1,y2)) -> False() eqZList(Z(),Z()) -> True() f(C(x1,x2)) -> C(f(x1),f(x2)) f(Z()) -> Z() first(C(x1,x2)) -> x1 g(x) -> x second(C(x1,x2)) -> x2 Signature: {and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0,Z/0} Obligation: Innermost basic terms: {and,eqZList,f,first,g,second}/{C,False,True,Z} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).