WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: A(C(z0,z1),z2,z3) -> c4(A(z0,z2,z3)) A(C(z0,z1),z2,z3) -> c5(A(z1,z2,z2)) A(Z(),z0,z1) -> c6() 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() FIRST(C(z0,z1)) -> c13() SECOND(C(z0,z1)) -> c12() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() a(C(z0,z1),z2,z3) -> C(a(z0,z2,z3),a(z1,z2,z2)) a(Z(),z0,z1) -> Z() 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() first(C(z0,z1)) -> z0 second(C(z0,z1)) -> z1 - Signature: {A/3,AND/2,EQZLIST/2,FIRST/1,SECOND/1,a/3,and/2,eqZList/2,first/1,second/1} / {C/2,False/0,True/0,Z/0,c/0 ,c1/0,c10/0,c11/0,c12/0,c13/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,AND,EQZLIST,FIRST,SECOND,a,and,eqZList,first ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,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: A(C(z0,z1),z2,z3) -> c4(A(z0,z2,z3)) A(C(z0,z1),z2,z3) -> c5(A(z1,z2,z2)) A(Z(),z0,z1) -> c6() 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() FIRST(C(z0,z1)) -> c13() SECOND(C(z0,z1)) -> c12() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() a(C(z0,z1),z2,z3) -> C(a(z0,z2,z3),a(z1,z2,z2)) a(Z(),z0,z1) -> Z() 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() first(C(z0,z1)) -> z0 second(C(z0,z1)) -> z1 - Signature: {A/3,AND/2,EQZLIST/2,FIRST/1,SECOND/1,a/3,and/2,eqZList/2,first/1,second/1} / {C/2,False/0,True/0,Z/0,c/0 ,c1/0,c10/0,c11/0,c12/0,c13/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,AND,EQZLIST,FIRST,SECOND,a,and,eqZList,first ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,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: A(C(z0,z1),z2,z3) -> c4(A(z0,z2,z3)) A(C(z0,z1),z2,z3) -> c5(A(z1,z2,z2)) A(Z(),z0,z1) -> c6() 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() FIRST(C(z0,z1)) -> c13() SECOND(C(z0,z1)) -> c12() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() a(C(z0,z1),z2,z3) -> C(a(z0,z2,z3),a(z1,z2,z2)) a(Z(),z0,z1) -> Z() 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() first(C(z0,z1)) -> z0 second(C(z0,z1)) -> z1 - Signature: {A/3,AND/2,EQZLIST/2,FIRST/1,SECOND/1,a/3,and/2,eqZList/2,first/1,second/1} / {C/2,False/0,True/0,Z/0,c/0 ,c1/0,c10/0,c11/0,c12/0,c13/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,AND,EQZLIST,FIRST,SECOND,a,and,eqZList,first ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: A(x,z,u){x -> C(x,y)} = A(C(x,y),z,u) ->^+ c4(A(x,z,u)) = C[A(x,z,u) = A(x,z,u){}] ** Step 1.b:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: A(C(z0,z1),z2,z3) -> c4(A(z0,z2,z3)) A(C(z0,z1),z2,z3) -> c5(A(z1,z2,z2)) A(Z(),z0,z1) -> c6() 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() FIRST(C(z0,z1)) -> c13() SECOND(C(z0,z1)) -> c12() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() a(C(z0,z1),z2,z3) -> C(a(z0,z2,z3),a(z1,z2,z2)) a(Z(),z0,z1) -> Z() 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() first(C(z0,z1)) -> z0 second(C(z0,z1)) -> z1 - Signature: {A/3,AND/2,EQZLIST/2,FIRST/1,SECOND/1,a/3,and/2,eqZList/2,first/1,second/1} / {C/2,False/0,True/0,Z/0,c/0 ,c1/0,c10/0,c11/0,c12/0,c13/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,AND,EQZLIST,FIRST,SECOND,a,and,eqZList,first ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: 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: {A,AND,EQZLIST,FIRST,SECOND,a,and,eqZList,first,second} TcT has computed the following interpretation: p(A) = [2] x1 + [2] x2 + [4] p(AND) = [1] x1 + [1] x2 + [2] p(C) = [1] x1 + [1] x2 + [4] p(EQZLIST) = [1] x1 + [1] x2 + [7] p(FIRST) = [7] p(False) = [0] p(SECOND) = [2] x1 + [0] p(True) = [0] p(Z) = [0] p(a) = [2] x1 + [2] p(and) = [4] x1 + [1] x2 + [0] p(c) = [2] p(c1) = [2] p(c10) = [0] p(c11) = [1] p(c12) = [1] p(c13) = [0] p(c2) = [1] p(c3) = [2] p(c4) = [1] x1 + [0] p(c5) = [1] x1 + [2] p(c6) = [2] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [1] x1 + [1] x2 + [6] p(c9) = [7] p(eqZList) = [0] p(first) = [2] x1 + [4] p(second) = [2] x1 + [5] Following rules are strictly oriented: A(C(z0,z1),z2,z3) = [2] z0 + [2] z1 + [2] z2 + [12] > [2] z0 + [2] z2 + [4] = c4(A(z0,z2,z3)) A(C(z0,z1),z2,z3) = [2] z0 + [2] z1 + [2] z2 + [12] > [2] z1 + [2] z2 + [6] = c5(A(z1,z2,z2)) A(Z(),z0,z1) = [2] z0 + [4] > [2] = c6() EQZLIST(C(z0,z1),C(z2,z3)) = [1] z0 + [1] z1 + [1] z2 + [1] z3 + [15] > [1] z0 + [1] z2 + [9] = c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),Z()) = [1] z0 + [1] z1 + [11] > [7] = c9() EQZLIST(Z(),C(z0,z1)) = [1] z0 + [1] z1 + [11] > [0] = c10() EQZLIST(Z(),Z()) = [7] > [1] = c11() FIRST(C(z0,z1)) = [7] > [0] = c13() SECOND(C(z0,z1)) = [2] z0 + [2] z1 + [8] > [1] = c12() Following rules are (at-least) weakly oriented: AND(False(),False()) = [2] >= [2] = c() AND(False(),True()) = [2] >= [1] = c2() AND(True(),False()) = [2] >= [2] = c1() AND(True(),True()) = [2] >= [2] = c3() EQZLIST(C(z0,z1),C(z2,z3)) = [1] z0 + [1] z1 + [1] z2 + [1] z3 + [15] >= [1] z1 + [1] z3 + [15] = c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) a(C(z0,z1),z2,z3) = [2] z0 + [2] z1 + [10] >= [2] z0 + [2] z1 + [8] = C(a(z0,z2,z3),a(z1,z2,z2)) a(Z(),z0,z1) = [2] >= [0] = Z() 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() first(C(z0,z1)) = [2] z0 + [2] z1 + [12] >= [1] z0 + [0] = z0 second(C(z0,z1)) = [2] z0 + [2] z1 + [13] >= [1] z1 + [0] = z1 ** Step 1.b:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: EQZLIST(C(z0,z1),C(z2,z3)) -> c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) - Weak TRS: A(C(z0,z1),z2,z3) -> c4(A(z0,z2,z3)) A(C(z0,z1),z2,z3) -> c5(A(z1,z2,z2)) A(Z(),z0,z1) -> c6() 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),Z()) -> c9() EQZLIST(Z(),C(z0,z1)) -> c10() EQZLIST(Z(),Z()) -> c11() FIRST(C(z0,z1)) -> c13() SECOND(C(z0,z1)) -> c12() a(C(z0,z1),z2,z3) -> C(a(z0,z2,z3),a(z1,z2,z2)) a(Z(),z0,z1) -> Z() 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() first(C(z0,z1)) -> z0 second(C(z0,z1)) -> z1 - Signature: {A/3,AND/2,EQZLIST/2,FIRST/1,SECOND/1,a/3,and/2,eqZList/2,first/1,second/1} / {C/2,False/0,True/0,Z/0,c/0 ,c1/0,c10/0,c11/0,c12/0,c13/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,AND,EQZLIST,FIRST,SECOND,a,and,eqZList,first ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: 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: {A,AND,EQZLIST,FIRST,SECOND,a,and,eqZList,first,second} TcT has computed the following interpretation: p(A) = [4] x1 + [0] p(AND) = [4] x1 + [4] x2 + [0] p(C) = [1] x1 + [1] x2 + [1] p(EQZLIST) = [1] x1 + [0] p(FIRST) = [3] x1 + [6] p(False) = [0] p(SECOND) = [4] p(True) = [0] p(Z) = [0] p(a) = [4] x1 + [0] p(and) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [4] p(c13) = [4] p(c2) = [0] p(c3) = [0] p(c4) = [1] x1 + [4] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [1] x1 + [1] x2 + [0] p(c9) = [1] p(eqZList) = [0] p(first) = [2] x1 + [2] p(second) = [1] x1 + [1] Following rules are strictly oriented: EQZLIST(C(z0,z1),C(z2,z3)) = [1] z0 + [1] z1 + [1] > [1] z1 + [0] = c8(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z1,z3)) Following rules are (at-least) weakly oriented: A(C(z0,z1),z2,z3) = [4] z0 + [4] z1 + [4] >= [4] z0 + [4] = c4(A(z0,z2,z3)) A(C(z0,z1),z2,z3) = [4] z0 + [4] z1 + [4] >= [4] z1 + [0] = c5(A(z1,z2,z2)) A(Z(),z0,z1) = [0] >= [0] = c6() 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] z0 + [1] z1 + [1] >= [1] z0 + [0] = c7(AND(eqZList(z0,z2),eqZList(z1,z3)),EQZLIST(z0,z2)) EQZLIST(C(z0,z1),Z()) = [1] z0 + [1] z1 + [1] >= [1] = c9() EQZLIST(Z(),C(z0,z1)) = [0] >= [0] = c10() EQZLIST(Z(),Z()) = [0] >= [0] = c11() FIRST(C(z0,z1)) = [3] z0 + [3] z1 + [9] >= [4] = c13() SECOND(C(z0,z1)) = [4] >= [4] = c12() a(C(z0,z1),z2,z3) = [4] z0 + [4] z1 + [4] >= [4] z0 + [4] z1 + [1] = C(a(z0,z2,z3),a(z1,z2,z2)) a(Z(),z0,z1) = [0] >= [0] = Z() 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() first(C(z0,z1)) = [2] z0 + [2] z1 + [4] >= [1] z0 + [0] = z0 second(C(z0,z1)) = [1] z0 + [1] z1 + [2] >= [1] z1 + [0] = z1 ** Step 1.b:3: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: A(C(z0,z1),z2,z3) -> c4(A(z0,z2,z3)) A(C(z0,z1),z2,z3) -> c5(A(z1,z2,z2)) A(Z(),z0,z1) -> c6() 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() FIRST(C(z0,z1)) -> c13() SECOND(C(z0,z1)) -> c12() a(C(z0,z1),z2,z3) -> C(a(z0,z2,z3),a(z1,z2,z2)) a(Z(),z0,z1) -> Z() 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() first(C(z0,z1)) -> z0 second(C(z0,z1)) -> z1 - Signature: {A/3,AND/2,EQZLIST/2,FIRST/1,SECOND/1,a/3,and/2,eqZList/2,first/1,second/1} / {C/2,False/0,True/0,Z/0,c/0 ,c1/0,c10/0,c11/0,c12/0,c13/0,c2/0,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,AND,EQZLIST,FIRST,SECOND,a,and,eqZList,first ,second} and constructors {C,False,True,Z,c,c1,c10,c11,c12,c13,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))