YES(O(1),O(n^1)) 0.00/0.96 YES(O(1),O(n^1)) 0.00/0.96 0.00/0.96 We are left with following problem, upon which TcT provides the 0.00/0.96 certificate YES(O(1),O(n^1)). 0.00/0.96 0.00/0.96 Strict Trs: 0.00/0.96 { a(Z(), y) -> Z() 0.00/0.96 , a(C(x1, x2), y) -> C(a(x1, y), a(x2, C(x1, x2))) 0.00/0.96 , second(C(x1, x2)) -> x2 0.00/0.96 , eqZList(Z(), Z()) -> True() 0.00/0.96 , eqZList(Z(), C(y1, y2)) -> False() 0.00/0.96 , eqZList(C(x1, x2), Z()) -> False() 0.00/0.96 , eqZList(C(x1, x2), C(y1, y2)) -> 0.00/0.96 and(eqZList(x1, y1), eqZList(x2, y2)) 0.00/0.96 , first(C(x1, x2)) -> x1 } 0.00/0.96 Weak Trs: 0.00/0.96 { and(True(), True()) -> True() 0.00/0.96 , and(True(), False()) -> False() 0.00/0.96 , and(False(), True()) -> False() 0.00/0.96 , and(False(), False()) -> False() } 0.00/0.96 Obligation: 0.00/0.96 innermost runtime complexity 0.00/0.96 Answer: 0.00/0.96 YES(O(1),O(n^1)) 0.00/0.96 0.00/0.96 The weightgap principle applies (using the following nonconstant 0.00/0.96 growth matrix-interpretation) 0.00/0.96 0.00/0.96 The following argument positions are usable: 0.00/0.96 Uargs(C) = {1, 2}, Uargs(and) = {1, 2} 0.00/0.96 0.00/0.96 TcT has computed the following matrix interpretation satisfying 0.00/0.96 not(EDA) and not(IDA(1)). 0.00/0.96 0.00/0.96 [a](x1, x2) = [1] x1 + [3] 0.00/0.96 0.00/0.96 [second](x1) = [1] x1 + [7] 0.00/0.96 0.00/0.96 [eqZList](x1, x2) = [1] x1 + [1] x2 + [1] 0.00/0.96 0.00/0.96 [Z] = [7] 0.00/0.96 0.00/0.96 [True] = [4] 0.00/0.96 0.00/0.96 [C](x1, x2) = [1] x1 + [1] x2 + [7] 0.00/0.96 0.00/0.96 [and](x1, x2) = [1] x1 + [1] x2 + [0] 0.00/0.96 0.00/0.96 [first](x1) = [1] x1 + [7] 0.00/0.96 0.00/0.96 [False] = [4] 0.00/0.96 0.00/0.96 The order satisfies the following ordering constraints: 0.00/0.96 0.00/0.96 [a(Z(), y)] = [10] 0.00/0.96 > [7] 0.00/0.96 = [Z()] 0.00/0.96 0.00/0.96 [a(C(x1, x2), y)] = [1] x1 + [1] x2 + [10] 0.00/0.96 ? [1] x1 + [1] x2 + [13] 0.00/0.96 = [C(a(x1, y), a(x2, C(x1, x2)))] 0.00/0.96 0.00/0.96 [second(C(x1, x2))] = [1] x1 + [1] x2 + [14] 0.00/0.96 > [1] x2 + [0] 0.00/0.96 = [x2] 0.00/0.96 0.00/0.96 [eqZList(Z(), Z())] = [15] 0.00/0.96 > [4] 0.00/0.96 = [True()] 0.00/0.96 0.00/0.96 [eqZList(Z(), C(y1, y2))] = [1] y1 + [1] y2 + [15] 0.00/0.96 > [4] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [eqZList(C(x1, x2), Z())] = [1] x1 + [1] x2 + [15] 0.00/0.96 > [4] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [eqZList(C(x1, x2), C(y1, y2))] = [1] x1 + [1] x2 + [1] y1 + [1] y2 + [15] 0.00/0.96 > [1] x1 + [1] x2 + [1] y1 + [1] y2 + [2] 0.00/0.96 = [and(eqZList(x1, y1), eqZList(x2, y2))] 0.00/0.96 0.00/0.96 [and(True(), True())] = [8] 0.00/0.96 > [4] 0.00/0.96 = [True()] 0.00/0.96 0.00/0.96 [and(True(), False())] = [8] 0.00/0.96 > [4] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [and(False(), True())] = [8] 0.00/0.96 > [4] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [and(False(), False())] = [8] 0.00/0.96 > [4] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [first(C(x1, x2))] = [1] x1 + [1] x2 + [14] 0.00/0.96 > [1] x1 + [0] 0.00/0.96 = [x1] 0.00/0.96 0.00/0.96 0.00/0.96 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.96 0.00/0.96 We are left with following problem, upon which TcT provides the 0.00/0.96 certificate YES(O(1),O(n^1)). 0.00/0.96 0.00/0.96 Strict Trs: { a(C(x1, x2), y) -> C(a(x1, y), a(x2, C(x1, x2))) } 0.00/0.96 Weak Trs: 0.00/0.96 { a(Z(), y) -> Z() 0.00/0.96 , second(C(x1, x2)) -> x2 0.00/0.96 , eqZList(Z(), Z()) -> True() 0.00/0.96 , eqZList(Z(), C(y1, y2)) -> False() 0.00/0.96 , eqZList(C(x1, x2), Z()) -> False() 0.00/0.96 , eqZList(C(x1, x2), C(y1, y2)) -> 0.00/0.96 and(eqZList(x1, y1), eqZList(x2, y2)) 0.00/0.96 , and(True(), True()) -> True() 0.00/0.96 , and(True(), False()) -> False() 0.00/0.96 , and(False(), True()) -> False() 0.00/0.96 , and(False(), False()) -> False() 0.00/0.96 , first(C(x1, x2)) -> x1 } 0.00/0.96 Obligation: 0.00/0.96 innermost runtime complexity 0.00/0.96 Answer: 0.00/0.96 YES(O(1),O(n^1)) 0.00/0.96 0.00/0.96 We use the processor 'matrix interpretation of dimension 1' to 0.00/0.96 orient following rules strictly. 0.00/0.96 0.00/0.96 Trs: { a(C(x1, x2), y) -> C(a(x1, y), a(x2, C(x1, x2))) } 0.00/0.96 0.00/0.96 The induced complexity on above rules (modulo remaining rules) is 0.00/0.96 YES(?,O(n^1)) . These rules are moved into the corresponding weak 0.00/0.96 component(s). 0.00/0.96 0.00/0.96 Sub-proof: 0.00/0.96 ---------- 0.00/0.96 The following argument positions are usable: 0.00/0.96 Uargs(C) = {1, 2}, Uargs(and) = {1, 2} 0.00/0.96 0.00/0.96 TcT has computed the following constructor-based matrix 0.00/0.96 interpretation satisfying not(EDA). 0.00/0.96 0.00/0.96 [a](x1, x2) = [2] x1 + [0] 0.00/0.96 0.00/0.96 [second](x1) = [3] x1 + [3] 0.00/0.96 0.00/0.96 [eqZList](x1, x2) = [0] 0.00/0.96 0.00/0.96 [Z] = [4] 0.00/0.96 0.00/0.96 [True] = [0] 0.00/0.96 0.00/0.96 [C](x1, x2) = [1] x1 + [1] x2 + [4] 0.00/0.96 0.00/0.96 [and](x1, x2) = [2] x1 + [1] x2 + [0] 0.00/0.96 0.00/0.96 [first](x1) = [3] x1 + [3] 0.00/0.96 0.00/0.96 [False] = [0] 0.00/0.96 0.00/0.96 The order satisfies the following ordering constraints: 0.00/0.96 0.00/0.96 [a(Z(), y)] = [8] 0.00/0.96 > [4] 0.00/0.96 = [Z()] 0.00/0.96 0.00/0.96 [a(C(x1, x2), y)] = [2] x1 + [2] x2 + [8] 0.00/0.96 > [2] x1 + [2] x2 + [4] 0.00/0.96 = [C(a(x1, y), a(x2, C(x1, x2)))] 0.00/0.96 0.00/0.96 [second(C(x1, x2))] = [3] x1 + [3] x2 + [15] 0.00/0.96 > [1] x2 + [0] 0.00/0.96 = [x2] 0.00/0.96 0.00/0.96 [eqZList(Z(), Z())] = [0] 0.00/0.96 >= [0] 0.00/0.96 = [True()] 0.00/0.96 0.00/0.96 [eqZList(Z(), C(y1, y2))] = [0] 0.00/0.96 >= [0] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [eqZList(C(x1, x2), Z())] = [0] 0.00/0.96 >= [0] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [eqZList(C(x1, x2), C(y1, y2))] = [0] 0.00/0.96 >= [0] 0.00/0.96 = [and(eqZList(x1, y1), eqZList(x2, y2))] 0.00/0.96 0.00/0.96 [and(True(), True())] = [0] 0.00/0.96 >= [0] 0.00/0.96 = [True()] 0.00/0.96 0.00/0.96 [and(True(), False())] = [0] 0.00/0.96 >= [0] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [and(False(), True())] = [0] 0.00/0.96 >= [0] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [and(False(), False())] = [0] 0.00/0.96 >= [0] 0.00/0.96 = [False()] 0.00/0.96 0.00/0.96 [first(C(x1, x2))] = [3] x1 + [3] x2 + [15] 0.00/0.96 > [1] x1 + [0] 0.00/0.96 = [x1] 0.00/0.96 0.00/0.96 0.00/0.96 We return to the main proof. 0.00/0.96 0.00/0.96 We are left with following problem, upon which TcT provides the 0.00/0.96 certificate YES(O(1),O(1)). 0.00/0.96 0.00/0.96 Weak Trs: 0.00/0.96 { a(Z(), y) -> Z() 0.00/0.96 , a(C(x1, x2), y) -> C(a(x1, y), a(x2, C(x1, x2))) 0.00/0.96 , second(C(x1, x2)) -> x2 0.00/0.96 , eqZList(Z(), Z()) -> True() 0.00/0.96 , eqZList(Z(), C(y1, y2)) -> False() 0.00/0.96 , eqZList(C(x1, x2), Z()) -> False() 0.00/0.96 , eqZList(C(x1, x2), C(y1, y2)) -> 0.00/0.96 and(eqZList(x1, y1), eqZList(x2, y2)) 0.00/0.96 , and(True(), True()) -> True() 0.00/0.96 , and(True(), False()) -> False() 0.00/0.96 , and(False(), True()) -> False() 0.00/0.96 , and(False(), False()) -> False() 0.00/0.96 , first(C(x1, x2)) -> x1 } 0.00/0.96 Obligation: 0.00/0.96 innermost runtime complexity 0.00/0.96 Answer: 0.00/0.96 YES(O(1),O(1)) 0.00/0.96 0.00/0.96 Empty rules are trivially bounded 0.00/0.96 0.00/0.96 Hurray, we answered YES(O(1),O(n^1)) 0.00/0.96 EOF