WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: EQZLIST(C(z0,z1),C(z2,z3)) -> c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) -> c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) -> c9() EQZLIST(Z(),C(z0,z1)) -> c10() EQZLIST(Z(),Z()) -> c11() F(C(z0,z1)) -> c4(F(z0)) F(C(z0,z1)) -> c5(F(z1)) F(Z()) -> c6() FIRST(C(z0,z1)) -> c13() G(z0) -> c14() SECOND(C(z0,z1)) -> c12() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqZList(C(z0,z1),C(z2,z3)) -> and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) -> False() eqZList(Z(),C(z0,z1)) -> False() eqZList(Z(),Z()) -> True() f(C(z0,z1)) -> C(f(z0),f(z1)) f(Z()) -> Z() first(C(z0,z1)) -> z0 g(z0) -> z0 second(C(z0,z1)) -> z1 - Signature: {AND/2,EQZLIST/2,F/1,FIRST/1,G/1,SECOND/1,and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0 ,Z/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EQZLIST(C(z0,z1),C(z2,z3)) -> c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) -> c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) -> c9() EQZLIST(Z(),C(z0,z1)) -> c10() EQZLIST(Z(),Z()) -> c11() F(C(z0,z1)) -> c4(F(z0)) F(C(z0,z1)) -> c5(F(z1)) F(Z()) -> c6() FIRST(C(z0,z1)) -> c13() G(z0) -> c14() SECOND(C(z0,z1)) -> c12() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqZList(C(z0,z1),C(z2,z3)) -> and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) -> False() eqZList(Z(),C(z0,z1)) -> False() eqZList(Z(),Z()) -> True() f(C(z0,z1)) -> C(f(z0),f(z1)) f(Z()) -> Z() first(C(z0,z1)) -> z0 g(z0) -> z0 second(C(z0,z1)) -> z1 - Signature: {AND/2,EQZLIST/2,F/1,FIRST/1,G/1,SECOND/1,and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0 ,Z/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EQZLIST(C(z0,z1),C(z2,z3)) -> c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) -> c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) -> c9() EQZLIST(Z(),C(z0,z1)) -> c10() EQZLIST(Z(),Z()) -> c11() F(C(z0,z1)) -> c4(F(z0)) F(C(z0,z1)) -> c5(F(z1)) F(Z()) -> c6() FIRST(C(z0,z1)) -> c13() G(z0) -> c14() SECOND(C(z0,z1)) -> c12() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqZList(C(z0,z1),C(z2,z3)) -> and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) -> False() eqZList(Z(),C(z0,z1)) -> False() eqZList(Z(),Z()) -> True() f(C(z0,z1)) -> C(f(z0),f(z1)) f(Z()) -> Z() first(C(z0,z1)) -> z0 g(z0) -> z0 second(C(z0,z1)) -> z1 - Signature: {AND/2,EQZLIST/2,F/1,FIRST/1,G/1,SECOND/1,and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0 ,Z/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: EQZLIST(x,z){x -> C(x,y),z -> C(z,u)} = EQZLIST(C(x,y),C(z,u)) ->^+ c7(AND(eqZList(x,z),eqZList(y,u)),EQZLIST(x,z)) = C[EQZLIST(x,z) = EQZLIST(x,z){}] ** Step 1.b:1: NaturalPI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: EQZLIST(C(z0,z1),C(z2,z3)) -> c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) -> c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) -> c9() EQZLIST(Z(),C(z0,z1)) -> c10() EQZLIST(Z(),Z()) -> c11() F(C(z0,z1)) -> c4(F(z0)) F(C(z0,z1)) -> c5(F(z1)) F(Z()) -> c6() FIRST(C(z0,z1)) -> c13() G(z0) -> c14() SECOND(C(z0,z1)) -> c12() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqZList(C(z0,z1),C(z2,z3)) -> and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) -> False() eqZList(Z(),C(z0,z1)) -> False() eqZList(Z(),Z()) -> True() f(C(z0,z1)) -> C(f(z0),f(z1)) f(Z()) -> Z() first(C(z0,z1)) -> z0 g(z0) -> z0 second(C(z0,z1)) -> z1 - Signature: {AND/2,EQZLIST/2,F/1,FIRST/1,G/1,SECOND/1,and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0 ,Z/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(AND) = {1,2}, uargs(C) = {1,2}, uargs(and) = {1,2}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c7) = {1,2}, uargs(c8) = {1,2} Following symbols are considered usable: {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g,second} TcT has computed the following interpretation: p(AND) = 3 + 2*x1 + 4*x2 p(C) = 2 + x1 + x2 p(EQZLIST) = 1 + 2*x1 + 2*x2 p(F) = 6 + x1 p(FIRST) = 4 p(False) = 0 p(G) = 0 p(SECOND) = 4*x1 p(True) = 0 p(Z) = 2 p(and) = x1 + 2*x2 p(c) = 0 p(c1) = 0 p(c10) = 0 p(c11) = 0 p(c12) = 4 p(c13) = 4 p(c14) = 0 p(c2) = 0 p(c3) = 0 p(c4) = x1 p(c5) = 2 + x1 p(c6) = 0 p(c7) = x1 + x2 p(c8) = 4 + x1 + x2 p(c9) = 0 p(eqZList) = 0 p(f) = 4*x1 p(first) = 3 + x1 p(g) = 1 + 5*x1 p(second) = 2*x1 Following rules are strictly oriented: EQZLIST(C(z0,z1),C(z2,z3)) = 9 + 2*z0 + 2*z1 + 2*z2 + 2*z3 > 4 + 2*z0 + 2*z2 = c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) = 9 + 2*z0 + 2*z1 + 2*z2 + 2*z3 > 8 + 2*z1 + 2*z3 = c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) = 9 + 2*z0 + 2*z1 > 0 = c9() EQZLIST(Z(),C(z0,z1)) = 9 + 2*z0 + 2*z1 > 0 = c10() EQZLIST(Z(),Z()) = 9 > 0 = c11() F(C(z0,z1)) = 8 + z0 + z1 > 6 + z0 = c4(F(z0)) F(Z()) = 8 > 0 = c6() SECOND(C(z0,z1)) = 8 + 4*z0 + 4*z1 > 4 = c12() Following rules are (at-least) weakly oriented: AND(False(),False()) = 3 >= 0 = c() AND(False(),True()) = 3 >= 0 = c2() AND(True(),False()) = 3 >= 0 = c1() AND(True(),True()) = 3 >= 0 = c3() F(C(z0,z1)) = 8 + z0 + z1 >= 8 + z1 = c5(F(z1)) FIRST(C(z0,z1)) = 4 >= 4 = c13() G(z0) = 0 >= 0 = c14() and(False(),False()) = 0 >= 0 = False() and(False(),True()) = 0 >= 0 = False() and(True(),False()) = 0 >= 0 = False() and(True(),True()) = 0 >= 0 = True() eqZList(C(z0,z1),C(z2,z3)) = 0 >= 0 = and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) = 0 >= 0 = False() eqZList(Z(),C(z0,z1)) = 0 >= 0 = False() eqZList(Z(),Z()) = 0 >= 0 = True() f(C(z0,z1)) = 8 + 4*z0 + 4*z1 >= 2 + 4*z0 + 4*z1 = C(f(z0),f(z1)) f(Z()) = 8 >= 2 = Z() first(C(z0,z1)) = 5 + z0 + z1 >= z0 = z0 g(z0) = 1 + 5*z0 >= z0 = z0 second(C(z0,z1)) = 4 + 2*z0 + 2*z1 >= z1 = z1 ** Step 1.b:2: NaturalPI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: F(C(z0,z1)) -> c5(F(z1)) FIRST(C(z0,z1)) -> c13() G(z0) -> c14() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() EQZLIST(C(z0,z1),C(z2,z3)) -> c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) -> c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) -> c9() EQZLIST(Z(),C(z0,z1)) -> c10() EQZLIST(Z(),Z()) -> c11() F(C(z0,z1)) -> c4(F(z0)) F(Z()) -> c6() SECOND(C(z0,z1)) -> c12() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqZList(C(z0,z1),C(z2,z3)) -> and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) -> False() eqZList(Z(),C(z0,z1)) -> False() eqZList(Z(),Z()) -> True() f(C(z0,z1)) -> C(f(z0),f(z1)) f(Z()) -> Z() first(C(z0,z1)) -> z0 g(z0) -> z0 second(C(z0,z1)) -> z1 - Signature: {AND/2,EQZLIST/2,F/1,FIRST/1,G/1,SECOND/1,and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0 ,Z/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(AND) = {1,2}, uargs(C) = {1,2}, uargs(and) = {1,2}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c7) = {1,2}, uargs(c8) = {1,2} Following symbols are considered usable: {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g,second} TcT has computed the following interpretation: p(AND) = x1 + 4*x2 p(C) = x1 + x2 p(EQZLIST) = 1 p(F) = 0 p(FIRST) = 2 p(False) = 0 p(G) = 7 + 2*x1 p(SECOND) = 4*x1 p(True) = 0 p(Z) = 0 p(and) = 4*x1 + 4*x2 p(c) = 0 p(c1) = 0 p(c10) = 1 p(c11) = 1 p(c12) = 0 p(c13) = 0 p(c14) = 3 p(c2) = 0 p(c3) = 0 p(c4) = x1 p(c5) = x1 p(c6) = 0 p(c7) = x1 + x2 p(c8) = x1 + x2 p(c9) = 0 p(eqZList) = 0 p(f) = 0 p(first) = 5*x1 p(g) = 4*x1 p(second) = x1 Following rules are strictly oriented: FIRST(C(z0,z1)) = 2 > 0 = c13() G(z0) = 7 + 2*z0 > 3 = c14() Following rules are (at-least) weakly oriented: AND(False(),False()) = 0 >= 0 = c() AND(False(),True()) = 0 >= 0 = c2() AND(True(),False()) = 0 >= 0 = c1() AND(True(),True()) = 0 >= 0 = c3() EQZLIST(C(z0,z1),C(z2,z3)) = 1 >= 1 = c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) = 1 >= 1 = c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) = 1 >= 0 = c9() EQZLIST(Z(),C(z0,z1)) = 1 >= 1 = c10() EQZLIST(Z(),Z()) = 1 >= 1 = c11() F(C(z0,z1)) = 0 >= 0 = c4(F(z0)) F(C(z0,z1)) = 0 >= 0 = c5(F(z1)) F(Z()) = 0 >= 0 = c6() SECOND(C(z0,z1)) = 4*z0 + 4*z1 >= 0 = c12() and(False(),False()) = 0 >= 0 = False() and(False(),True()) = 0 >= 0 = False() and(True(),False()) = 0 >= 0 = False() and(True(),True()) = 0 >= 0 = True() eqZList(C(z0,z1),C(z2,z3)) = 0 >= 0 = and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) = 0 >= 0 = False() eqZList(Z(),C(z0,z1)) = 0 >= 0 = False() eqZList(Z(),Z()) = 0 >= 0 = True() f(C(z0,z1)) = 0 >= 0 = C(f(z0),f(z1)) f(Z()) = 0 >= 0 = Z() first(C(z0,z1)) = 5*z0 + 5*z1 >= z0 = z0 g(z0) = 4*z0 >= z0 = z0 second(C(z0,z1)) = z0 + z1 >= z1 = z1 ** Step 1.b:3: NaturalPI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: F(C(z0,z1)) -> c5(F(z1)) - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() EQZLIST(C(z0,z1),C(z2,z3)) -> c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) -> c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) -> c9() EQZLIST(Z(),C(z0,z1)) -> c10() EQZLIST(Z(),Z()) -> c11() F(C(z0,z1)) -> c4(F(z0)) F(Z()) -> c6() FIRST(C(z0,z1)) -> c13() G(z0) -> c14() SECOND(C(z0,z1)) -> c12() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqZList(C(z0,z1),C(z2,z3)) -> and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) -> False() eqZList(Z(),C(z0,z1)) -> False() eqZList(Z(),Z()) -> True() f(C(z0,z1)) -> C(f(z0),f(z1)) f(Z()) -> Z() first(C(z0,z1)) -> z0 g(z0) -> z0 second(C(z0,z1)) -> z1 - Signature: {AND/2,EQZLIST/2,F/1,FIRST/1,G/1,SECOND/1,and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0 ,Z/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(AND) = {1,2}, uargs(C) = {1,2}, uargs(and) = {1,2}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c7) = {1,2}, uargs(c8) = {1,2} Following symbols are considered usable: {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g,second} TcT has computed the following interpretation: p(AND) = 3 + x1 + 4*x2 p(C) = 1 + x1 + x2 p(EQZLIST) = 1 + 5*x1 + 4*x2 p(F) = 2 + 2*x1 p(FIRST) = 2 + 4*x1 p(False) = 0 p(G) = x1 p(SECOND) = 0 p(True) = 0 p(Z) = 0 p(and) = 2*x1 + x2 p(c) = 3 p(c1) = 3 p(c10) = 0 p(c11) = 0 p(c12) = 0 p(c13) = 2 p(c14) = 0 p(c2) = 0 p(c3) = 0 p(c4) = x1 p(c5) = x1 p(c6) = 2 p(c7) = 6 + x1 + x2 p(c8) = 1 + x1 + x2 p(c9) = 6 p(eqZList) = 0 p(f) = 3 + 4*x1 p(first) = 4 + x1 p(g) = 1 + 4*x1 p(second) = 2 + 4*x1 Following rules are strictly oriented: F(C(z0,z1)) = 4 + 2*z0 + 2*z1 > 2 + 2*z1 = c5(F(z1)) Following rules are (at-least) weakly oriented: AND(False(),False()) = 3 >= 3 = c() AND(False(),True()) = 3 >= 0 = c2() AND(True(),False()) = 3 >= 3 = c1() AND(True(),True()) = 3 >= 0 = c3() EQZLIST(C(z0,z1),C(z2,z3)) = 10 + 5*z0 + 5*z1 + 4*z2 + 4*z3 >= 10 + 5*z0 + 4*z2 = c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) = 10 + 5*z0 + 5*z1 + 4*z2 + 4*z3 >= 5 + 5*z1 + 4*z3 = c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) = 6 + 5*z0 + 5*z1 >= 6 = c9() EQZLIST(Z(),C(z0,z1)) = 5 + 4*z0 + 4*z1 >= 0 = c10() EQZLIST(Z(),Z()) = 1 >= 0 = c11() F(C(z0,z1)) = 4 + 2*z0 + 2*z1 >= 2 + 2*z0 = c4(F(z0)) F(Z()) = 2 >= 2 = c6() FIRST(C(z0,z1)) = 6 + 4*z0 + 4*z1 >= 2 = c13() G(z0) = z0 >= 0 = c14() SECOND(C(z0,z1)) = 0 >= 0 = c12() and(False(),False()) = 0 >= 0 = False() and(False(),True()) = 0 >= 0 = False() and(True(),False()) = 0 >= 0 = False() and(True(),True()) = 0 >= 0 = True() eqZList(C(z0,z1),C(z2,z3)) = 0 >= 0 = and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) = 0 >= 0 = False() eqZList(Z(),C(z0,z1)) = 0 >= 0 = False() eqZList(Z(),Z()) = 0 >= 0 = True() f(C(z0,z1)) = 7 + 4*z0 + 4*z1 >= 7 + 4*z0 + 4*z1 = C(f(z0),f(z1)) f(Z()) = 3 >= 0 = Z() first(C(z0,z1)) = 5 + z0 + z1 >= z0 = z0 g(z0) = 1 + 4*z0 >= z0 = z0 second(C(z0,z1)) = 6 + 4*z0 + 4*z1 >= z1 = z1 ** Step 1.b:4: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() EQZLIST(C(z0,z1),C(z2,z3)) -> c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),C(z2,z3)) -> c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) EQZLIST(C(z0,z1),Z()) -> c9() EQZLIST(Z(),C(z0,z1)) -> c10() EQZLIST(Z(),Z()) -> c11() F(C(z0,z1)) -> c4(F(z0)) F(C(z0,z1)) -> c5(F(z1)) F(Z()) -> c6() FIRST(C(z0,z1)) -> c13() G(z0) -> c14() SECOND(C(z0,z1)) -> c12() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqZList(C(z0,z1),C(z2,z3)) -> and(eqZList(z0,z2),eqZList(z1,z3)) eqZList(C(z0,z1),Z()) -> False() eqZList(Z(),C(z0,z1)) -> False() eqZList(Z(),Z()) -> True() f(C(z0,z1)) -> C(f(z0),f(z1)) f(Z()) -> Z() first(C(z0,z1)) -> z0 g(z0) -> z0 second(C(z0,z1)) -> z1 - Signature: {AND/2,EQZLIST/2,F/1,FIRST/1,G/1,SECOND/1,and/2,eqZList/2,f/1,first/1,g/1,second/1} / {C/2,False/0,True/0 ,Z/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EQZLIST,F,FIRST,G,SECOND,and,eqZList,f,first,g ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))