YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { a(Z(), y, z) -> Z() , a(C(x1, x2), y, z) -> C(a(x1, y, z), a(x2, y, y)) , second(C(x1, x2)) -> x2 , eqZList(Z(), Z()) -> True() , eqZList(Z(), C(y1, y2)) -> False() , eqZList(C(x1, x2), Z()) -> False() , eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2)) , first(C(x1, x2)) -> x1 } Weak Trs: { and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following innermost weak dependency pairs: Strict DPs: { a^#(Z(), y, z) -> c_1() , a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) , second^#(C(x1, x2)) -> c_3() , eqZList^#(Z(), Z()) -> c_4() , eqZList^#(Z(), C(y1, y2)) -> c_5() , eqZList^#(C(x1, x2), Z()) -> c_6() , eqZList^#(C(x1, x2), C(y1, y2)) -> c_7(and^#(eqZList(x1, y1), eqZList(x2, y2))) , first^#(C(x1, x2)) -> c_8() } Weak DPs: { and^#(True(), True()) -> c_9() , and^#(True(), False()) -> c_10() , and^#(False(), True()) -> c_11() , and^#(False(), False()) -> c_12() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a^#(Z(), y, z) -> c_1() , a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) , second^#(C(x1, x2)) -> c_3() , eqZList^#(Z(), Z()) -> c_4() , eqZList^#(Z(), C(y1, y2)) -> c_5() , eqZList^#(C(x1, x2), Z()) -> c_6() , eqZList^#(C(x1, x2), C(y1, y2)) -> c_7(and^#(eqZList(x1, y1), eqZList(x2, y2))) , first^#(C(x1, x2)) -> c_8() } Strict Trs: { a(Z(), y, z) -> Z() , a(C(x1, x2), y, z) -> C(a(x1, y, z), a(x2, y, y)) , second(C(x1, x2)) -> x2 , eqZList(Z(), Z()) -> True() , eqZList(Z(), C(y1, y2)) -> False() , eqZList(C(x1, x2), Z()) -> False() , eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2)) , first(C(x1, x2)) -> x1 } Weak DPs: { and^#(True(), True()) -> c_9() , and^#(True(), False()) -> c_10() , and^#(False(), True()) -> c_11() , and^#(False(), False()) -> c_12() } Weak Trs: { and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Strict Usable Rules: { eqZList(Z(), Z()) -> True() , eqZList(Z(), C(y1, y2)) -> False() , eqZList(C(x1, x2), Z()) -> False() , eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2)) } Weak Usable Rules: { and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a^#(Z(), y, z) -> c_1() , a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) , second^#(C(x1, x2)) -> c_3() , eqZList^#(Z(), Z()) -> c_4() , eqZList^#(Z(), C(y1, y2)) -> c_5() , eqZList^#(C(x1, x2), Z()) -> c_6() , eqZList^#(C(x1, x2), C(y1, y2)) -> c_7(and^#(eqZList(x1, y1), eqZList(x2, y2))) , first^#(C(x1, x2)) -> c_8() } Strict Trs: { eqZList(Z(), Z()) -> True() , eqZList(Z(), C(y1, y2)) -> False() , eqZList(C(x1, x2), Z()) -> False() , eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2)) } Weak DPs: { and^#(True(), True()) -> c_9() , and^#(True(), False()) -> c_10() , and^#(False(), True()) -> c_11() , and^#(False(), False()) -> c_12() } Weak Trs: { and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(and) = {1, 2}, Uargs(c_2) = {1, 2}, Uargs(c_7) = {1}, Uargs(and^#) = {1, 2} TcT has computed the following constructor-restricted matrix interpretation. [eqZList](x1, x2) = [1 1] x1 + [1] [0 0] [1] [Z] = [0] [0] [True] = [0] [0] [C](x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 1] [0 1] [2] [and](x1, x2) = [1 0] x1 + [1 2] x2 + [0] [0 0] [0 0] [0] [False] = [0] [0] [a^#](x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [2] [1 1] [1 1] [2 2] [2] [c_1] = [1] [1] [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 1] [0 1] [2] [second^#](x1) = [1 1] x1 + [2] [1 1] [2] [c_3] = [1] [1] [eqZList^#](x1, x2) = [1 1] x1 + [0] [0 0] [0] [c_4] = [1] [1] [c_5] = [1] [0] [c_6] = [1] [0] [c_7](x1) = [1 0] x1 + [1] [0 1] [2] [and^#](x1, x2) = [1 2] x1 + [1 1] x2 + [0] [0 0] [0 0] [0] [first^#](x1) = [1 1] x1 + [2] [1 1] [2] [c_8] = [1] [1] [c_9] = [0] [0] [c_10] = [0] [0] [c_11] = [0] [0] [c_12] = [0] [0] The following symbols are considered usable {eqZList, and, a^#, second^#, eqZList^#, and^#, first^#} The order satisfies the following ordering constraints: [eqZList(Z(), Z())] = [1] [1] > [0] [0] = [True()] [eqZList(Z(), C(y1, y2))] = [1] [1] > [0] [0] = [False()] [eqZList(C(x1, x2), Z())] = [1 1] x1 + [1 1] x2 + [5] [0 0] [0 0] [1] > [0] [0] = [False()] [eqZList(C(x1, x2), C(y1, y2))] = [1 1] x1 + [1 1] x2 + [5] [0 0] [0 0] [1] > [1 1] x1 + [1 1] x2 + [4] [0 0] [0 0] [0] = [and(eqZList(x1, y1), eqZList(x2, y2))] [and(True(), True())] = [0] [0] >= [0] [0] = [True()] [and(True(), False())] = [0] [0] >= [0] [0] = [False()] [and(False(), True())] = [0] [0] >= [0] [0] = [False()] [and(False(), False())] = [0] [0] >= [0] [0] = [False()] [a^#(Z(), y, z)] = [0 0] y + [0 0] z + [2] [1 1] [2 2] [2] > [1] [1] = [c_1()] [a^#(C(x1, x2), y, z)] = [0 0] x1 + [0 0] x2 + [0 0] y + [0 0] z + [2] [1 1] [1 1] [1 1] [2 2] [6] ? [0 0] x1 + [0 0] x2 + [0 0] y + [0 0] z + [6] [1 1] [1 1] [4 4] [2 2] [6] = [c_2(a^#(x1, y, z), a^#(x2, y, y))] [second^#(C(x1, x2))] = [1 1] x1 + [1 1] x2 + [6] [1 1] [1 1] [6] > [1] [1] = [c_3()] [eqZList^#(Z(), Z())] = [0] [0] ? [1] [1] = [c_4()] [eqZList^#(Z(), C(y1, y2))] = [0] [0] ? [1] [0] = [c_5()] [eqZList^#(C(x1, x2), Z())] = [1 1] x1 + [1 1] x2 + [4] [0 0] [0 0] [0] > [1] [0] = [c_6()] [eqZList^#(C(x1, x2), C(y1, y2))] = [1 1] x1 + [1 1] x2 + [4] [0 0] [0 0] [0] ? [1 1] x1 + [1 1] x2 + [6] [0 0] [0 0] [2] = [c_7(and^#(eqZList(x1, y1), eqZList(x2, y2)))] [and^#(True(), True())] = [0] [0] >= [0] [0] = [c_9()] [and^#(True(), False())] = [0] [0] >= [0] [0] = [c_10()] [and^#(False(), True())] = [0] [0] >= [0] [0] = [c_11()] [and^#(False(), False())] = [0] [0] >= [0] [0] = [c_12()] [first^#(C(x1, x2))] = [1 1] x1 + [1 1] x2 + [6] [1 1] [1 1] [6] > [1] [1] = [c_8()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) , eqZList^#(Z(), Z()) -> c_4() , eqZList^#(Z(), C(y1, y2)) -> c_5() , eqZList^#(C(x1, x2), C(y1, y2)) -> c_7(and^#(eqZList(x1, y1), eqZList(x2, y2))) } Weak DPs: { a^#(Z(), y, z) -> c_1() , second^#(C(x1, x2)) -> c_3() , eqZList^#(C(x1, x2), Z()) -> c_6() , and^#(True(), True()) -> c_9() , and^#(True(), False()) -> c_10() , and^#(False(), True()) -> c_11() , and^#(False(), False()) -> c_12() , first^#(C(x1, x2)) -> c_8() } Weak Trs: { eqZList(Z(), Z()) -> True() , eqZList(Z(), C(y1, y2)) -> False() , eqZList(C(x1, x2), Z()) -> False() , eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {2,3,4} by applications of Pre({2,3,4}) = {}. Here rules are labeled as follows: DPs: { 1: a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) , 2: eqZList^#(Z(), Z()) -> c_4() , 3: eqZList^#(Z(), C(y1, y2)) -> c_5() , 4: eqZList^#(C(x1, x2), C(y1, y2)) -> c_7(and^#(eqZList(x1, y1), eqZList(x2, y2))) , 5: a^#(Z(), y, z) -> c_1() , 6: second^#(C(x1, x2)) -> c_3() , 7: eqZList^#(C(x1, x2), Z()) -> c_6() , 8: and^#(True(), True()) -> c_9() , 9: and^#(True(), False()) -> c_10() , 10: and^#(False(), True()) -> c_11() , 11: and^#(False(), False()) -> c_12() , 12: first^#(C(x1, x2)) -> c_8() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) } Weak DPs: { a^#(Z(), y, z) -> c_1() , second^#(C(x1, x2)) -> c_3() , eqZList^#(Z(), Z()) -> c_4() , eqZList^#(Z(), C(y1, y2)) -> c_5() , eqZList^#(C(x1, x2), Z()) -> c_6() , eqZList^#(C(x1, x2), C(y1, y2)) -> c_7(and^#(eqZList(x1, y1), eqZList(x2, y2))) , and^#(True(), True()) -> c_9() , and^#(True(), False()) -> c_10() , and^#(False(), True()) -> c_11() , and^#(False(), False()) -> c_12() , first^#(C(x1, x2)) -> c_8() } Weak Trs: { eqZList(Z(), Z()) -> True() , eqZList(Z(), C(y1, y2)) -> False() , eqZList(C(x1, x2), Z()) -> False() , eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { a^#(Z(), y, z) -> c_1() , second^#(C(x1, x2)) -> c_3() , eqZList^#(Z(), Z()) -> c_4() , eqZList^#(Z(), C(y1, y2)) -> c_5() , eqZList^#(C(x1, x2), Z()) -> c_6() , eqZList^#(C(x1, x2), C(y1, y2)) -> c_7(and^#(eqZList(x1, y1), eqZList(x2, y2))) , and^#(True(), True()) -> c_9() , and^#(True(), False()) -> c_10() , and^#(False(), True()) -> c_11() , and^#(False(), False()) -> c_12() , first^#(C(x1, x2)) -> c_8() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) } Weak Trs: { eqZList(Z(), Z()) -> True() , eqZList(Z(), C(y1, y2)) -> False() , eqZList(C(x1, x2), Z()) -> False() , eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_2) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [a](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [second](x1) = [7] x1 + [0] [eqZList](x1, x2) = [7] x1 + [7] x2 + [0] [Z] = [0] [True] = [0] [C](x1, x2) = [1] x1 + [1] x2 + [1] [and](x1, x2) = [7] x1 + [7] x2 + [0] [first](x1) = [7] x1 + [0] [False] = [0] [a^#](x1, x2, x3) = [4] x1 + [0] [c_1] = [0] [c_2](x1, x2) = [1] x1 + [1] x2 + [1] [second^#](x1) = [7] x1 + [0] [c_3] = [0] [eqZList^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_4] = [0] [c_5] = [0] [c_6] = [0] [c_7](x1) = [7] x1 + [0] [and^#](x1, x2) = [7] x1 + [7] x2 + [0] [first^#](x1) = [7] x1 + [0] [c_8] = [0] [c_9] = [0] [c_10] = [0] [c_11] = [0] [c_12] = [0] The following symbols are considered usable {a^#} The order satisfies the following ordering constraints: [a^#(C(x1, x2), y, z)] = [4] x1 + [4] x2 + [4] > [4] x1 + [4] x2 + [1] = [c_2(a^#(x1, y, z), a^#(x2, y, y))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { a^#(C(x1, x2), y, z) -> c_2(a^#(x1, y, z), a^#(x2, y, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))