YES(O(1),O(n^2)) 175.69/60.06 YES(O(1),O(n^2)) 175.69/60.06 175.69/60.06 We are left with following problem, upon which TcT provides the 175.69/60.06 certificate YES(O(1),O(n^2)). 175.69/60.06 175.69/60.06 Strict Trs: 175.69/60.06 { a__zeros() -> cons(0(), zeros()) 175.69/60.06 , a__zeros() -> zeros() 175.69/60.06 , a__tail(X) -> tail(X) 175.69/60.06 , a__tail(cons(X, XS)) -> mark(XS) 175.69/60.06 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 175.69/60.06 , mark(0()) -> 0() 175.69/60.06 , mark(zeros()) -> a__zeros() 175.69/60.06 , mark(tail(X)) -> a__tail(mark(X)) } 175.69/60.06 Obligation: 175.69/60.06 derivational complexity 175.69/60.06 Answer: 175.69/60.06 YES(O(1),O(n^2)) 175.69/60.06 175.69/60.06 The weightgap principle applies (using the following nonconstant 175.69/60.06 growth matrix-interpretation) 175.69/60.06 175.69/60.06 TcT has computed the following triangular matrix interpretation. 175.69/60.06 Note that the diagonal of the component-wise maxima of 175.69/60.06 interpretation-entries contains no more than 1 non-zero entries. 175.69/60.06 175.69/60.06 [a__zeros] = [2] 175.69/60.06 175.69/60.06 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 175.69/60.06 175.69/60.06 [0] = [0] 175.69/60.06 175.69/60.06 [zeros] = [0] 175.69/60.06 175.69/60.06 [a__tail](x1) = [1] x1 + [0] 175.69/60.06 175.69/60.06 [mark](x1) = [1] x1 + [0] 175.69/60.06 175.69/60.06 [tail](x1) = [1] x1 + [1] 175.69/60.06 175.69/60.06 The order satisfies the following ordering constraints: 175.69/60.06 175.69/60.06 [a__zeros()] = [2] 175.69/60.06 > [0] 175.69/60.06 = [cons(0(), zeros())] 175.69/60.06 175.69/60.06 [a__zeros()] = [2] 175.69/60.06 > [0] 175.69/60.06 = [zeros()] 175.69/60.06 175.69/60.06 [a__tail(X)] = [1] X + [0] 175.69/60.06 ? [1] X + [1] 175.69/60.06 = [tail(X)] 175.69/60.06 175.69/60.06 [a__tail(cons(X, XS))] = [1] X + [1] XS + [0] 175.69/60.06 >= [1] XS + [0] 175.69/60.06 = [mark(XS)] 175.69/60.06 175.69/60.06 [mark(cons(X1, X2))] = [1] X1 + [1] X2 + [0] 175.69/60.06 >= [1] X1 + [1] X2 + [0] 175.69/60.06 = [cons(mark(X1), X2)] 175.69/60.06 175.69/60.06 [mark(0())] = [0] 175.69/60.06 >= [0] 175.69/60.06 = [0()] 175.69/60.06 175.69/60.06 [mark(zeros())] = [0] 175.69/60.06 ? [2] 175.69/60.06 = [a__zeros()] 175.69/60.06 175.69/60.06 [mark(tail(X))] = [1] X + [1] 175.69/60.06 > [1] X + [0] 175.69/60.06 = [a__tail(mark(X))] 175.69/60.06 175.69/60.06 175.69/60.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 175.69/60.06 175.69/60.06 We are left with following problem, upon which TcT provides the 175.69/60.06 certificate YES(O(1),O(n^2)). 175.69/60.06 175.69/60.06 Strict Trs: 175.69/60.06 { a__tail(X) -> tail(X) 175.69/60.06 , a__tail(cons(X, XS)) -> mark(XS) 175.69/60.06 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 175.69/60.06 , mark(0()) -> 0() 175.69/60.06 , mark(zeros()) -> a__zeros() } 175.69/60.06 Weak Trs: 175.69/60.06 { a__zeros() -> cons(0(), zeros()) 175.69/60.06 , a__zeros() -> zeros() 175.69/60.06 , mark(tail(X)) -> a__tail(mark(X)) } 175.69/60.06 Obligation: 175.69/60.06 derivational complexity 175.69/60.06 Answer: 175.69/60.06 YES(O(1),O(n^2)) 175.69/60.06 175.69/60.06 We use the processor 'matrix interpretation of dimension 1' to 175.69/60.06 orient following rules strictly. 175.69/60.06 175.69/60.06 Trs: { a__tail(cons(X, XS)) -> mark(XS) } 175.69/60.06 175.69/60.06 The induced complexity on above rules (modulo remaining rules) is 175.69/60.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 175.69/60.06 component(s). 175.69/60.06 175.69/60.06 Sub-proof: 175.69/60.06 ---------- 175.69/60.06 TcT has computed the following triangular matrix interpretation. 175.69/60.06 175.69/60.06 [a__zeros] = [0] 175.69/60.06 175.69/60.06 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 175.69/60.06 175.69/60.06 [0] = [0] 175.69/60.06 175.69/60.06 [zeros] = [0] 175.69/60.06 175.69/60.06 [a__tail](x1) = [1] x1 + [1] 175.69/60.06 175.69/60.06 [mark](x1) = [1] x1 + [0] 175.69/60.06 175.69/60.06 [tail](x1) = [1] x1 + [1] 175.69/60.06 175.69/60.06 The order satisfies the following ordering constraints: 175.69/60.06 175.69/60.06 [a__zeros()] = [0] 175.69/60.06 >= [0] 175.69/60.06 = [cons(0(), zeros())] 175.69/60.06 175.69/60.06 [a__zeros()] = [0] 175.69/60.06 >= [0] 175.69/60.06 = [zeros()] 175.69/60.06 175.69/60.06 [a__tail(X)] = [1] X + [1] 175.69/60.06 >= [1] X + [1] 175.69/60.06 = [tail(X)] 175.69/60.06 175.69/60.06 [a__tail(cons(X, XS))] = [1] X + [1] XS + [1] 175.69/60.06 > [1] XS + [0] 175.69/60.06 = [mark(XS)] 175.69/60.06 175.69/60.06 [mark(cons(X1, X2))] = [1] X1 + [1] X2 + [0] 175.69/60.06 >= [1] X1 + [1] X2 + [0] 175.69/60.06 = [cons(mark(X1), X2)] 175.69/60.06 175.69/60.06 [mark(0())] = [0] 175.69/60.06 >= [0] 175.69/60.06 = [0()] 175.69/60.06 175.69/60.06 [mark(zeros())] = [0] 175.69/60.06 >= [0] 175.69/60.06 = [a__zeros()] 175.69/60.06 175.69/60.06 [mark(tail(X))] = [1] X + [1] 175.69/60.06 >= [1] X + [1] 175.69/60.06 = [a__tail(mark(X))] 175.69/60.06 175.69/60.06 175.69/60.06 We return to the main proof. 175.69/60.06 175.69/60.06 We are left with following problem, upon which TcT provides the 175.69/60.06 certificate YES(O(1),O(n^2)). 175.69/60.06 175.69/60.06 Strict Trs: 175.69/60.06 { a__tail(X) -> tail(X) 175.69/60.06 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 175.69/60.06 , mark(0()) -> 0() 175.69/60.06 , mark(zeros()) -> a__zeros() } 175.69/60.06 Weak Trs: 175.69/60.06 { a__zeros() -> cons(0(), zeros()) 175.69/60.06 , a__zeros() -> zeros() 175.69/60.06 , a__tail(cons(X, XS)) -> mark(XS) 175.69/60.06 , mark(tail(X)) -> a__tail(mark(X)) } 175.69/60.06 Obligation: 175.69/60.06 derivational complexity 175.69/60.06 Answer: 175.69/60.06 YES(O(1),O(n^2)) 175.69/60.06 175.69/60.06 We use the processor 'matrix interpretation of dimension 1' to 175.69/60.06 orient following rules strictly. 175.69/60.06 175.69/60.06 Trs: 175.69/60.06 { mark(0()) -> 0() 175.69/60.06 , mark(zeros()) -> a__zeros() } 175.69/60.06 175.69/60.06 The induced complexity on above rules (modulo remaining rules) is 175.69/60.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 175.69/60.06 component(s). 175.69/60.06 175.69/60.06 Sub-proof: 175.69/60.06 ---------- 175.69/60.06 TcT has computed the following triangular matrix interpretation. 175.69/60.06 175.69/60.06 [a__zeros] = [0] 175.69/60.06 175.69/60.06 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 175.69/60.06 175.69/60.06 [0] = [0] 175.69/60.06 175.69/60.06 [zeros] = [0] 175.69/60.06 175.69/60.06 [a__tail](x1) = [1] x1 + [2] 175.69/60.06 175.69/60.06 [mark](x1) = [1] x1 + [1] 175.69/60.06 175.69/60.06 [tail](x1) = [1] x1 + [2] 175.69/60.06 175.69/60.06 The order satisfies the following ordering constraints: 175.69/60.06 175.69/60.06 [a__zeros()] = [0] 175.69/60.06 >= [0] 175.69/60.06 = [cons(0(), zeros())] 175.69/60.06 175.69/60.06 [a__zeros()] = [0] 175.69/60.06 >= [0] 175.69/60.06 = [zeros()] 175.69/60.06 175.69/60.06 [a__tail(X)] = [1] X + [2] 175.69/60.06 >= [1] X + [2] 175.69/60.06 = [tail(X)] 175.69/60.06 175.69/60.06 [a__tail(cons(X, XS))] = [1] X + [1] XS + [2] 175.69/60.06 > [1] XS + [1] 175.69/60.06 = [mark(XS)] 175.69/60.06 175.69/60.06 [mark(cons(X1, X2))] = [1] X1 + [1] X2 + [1] 175.69/60.06 >= [1] X1 + [1] X2 + [1] 175.69/60.06 = [cons(mark(X1), X2)] 175.69/60.06 175.69/60.06 [mark(0())] = [1] 175.69/60.06 > [0] 175.69/60.06 = [0()] 175.69/60.06 175.69/60.06 [mark(zeros())] = [1] 175.69/60.06 > [0] 175.69/60.06 = [a__zeros()] 175.69/60.06 175.69/60.06 [mark(tail(X))] = [1] X + [3] 175.69/60.06 >= [1] X + [3] 175.69/60.06 = [a__tail(mark(X))] 175.69/60.06 175.69/60.06 175.69/60.06 We return to the main proof. 175.69/60.06 175.69/60.06 We are left with following problem, upon which TcT provides the 175.69/60.06 certificate YES(O(1),O(n^2)). 175.69/60.06 175.69/60.06 Strict Trs: 175.69/60.06 { a__tail(X) -> tail(X) 175.69/60.06 , mark(cons(X1, X2)) -> cons(mark(X1), X2) } 175.69/60.06 Weak Trs: 175.69/60.06 { a__zeros() -> cons(0(), zeros()) 175.69/60.06 , a__zeros() -> zeros() 175.69/60.06 , a__tail(cons(X, XS)) -> mark(XS) 175.69/60.06 , mark(0()) -> 0() 175.69/60.06 , mark(zeros()) -> a__zeros() 175.69/60.06 , mark(tail(X)) -> a__tail(mark(X)) } 175.69/60.06 Obligation: 175.69/60.06 derivational complexity 175.69/60.06 Answer: 175.69/60.06 YES(O(1),O(n^2)) 175.69/60.06 175.69/60.06 We use the processor 'matrix interpretation of dimension 2' to 175.69/60.06 orient following rules strictly. 175.69/60.06 175.69/60.06 Trs: { a__tail(X) -> tail(X) } 175.69/60.06 175.69/60.06 The induced complexity on above rules (modulo remaining rules) is 175.69/60.06 YES(?,O(n^2)) . These rules are moved into the corresponding weak 175.69/60.06 component(s). 175.69/60.06 175.69/60.06 Sub-proof: 175.69/60.06 ---------- 175.69/60.06 TcT has computed the following triangular matrix interpretation. 175.69/60.06 175.69/60.06 [a__zeros] = [0] 175.69/60.06 [0] 175.69/60.06 175.69/60.06 [cons](x1, x2) = [1 0] x1 + [1 2] x2 + [0] 175.69/60.06 [0 1] [0 1] [0] 175.69/60.06 175.69/60.06 [0] = [0] 175.69/60.06 [0] 175.69/60.06 175.69/60.06 [zeros] = [0] 175.69/60.06 [0] 175.69/60.06 175.69/60.06 [a__tail](x1) = [1 0] x1 + [1] 175.69/60.06 [0 1] [1] 175.69/60.06 175.69/60.06 [mark](x1) = [1 1] x1 + [0] 175.69/60.06 [0 1] [0] 175.69/60.06 175.69/60.06 [tail](x1) = [1 0] x1 + [0] 175.69/60.06 [0 1] [1] 175.69/60.06 175.69/60.06 The order satisfies the following ordering constraints: 175.69/60.06 175.69/60.06 [a__zeros()] = [0] 175.69/60.06 [0] 175.69/60.06 >= [0] 175.69/60.06 [0] 175.69/60.06 = [cons(0(), zeros())] 175.69/60.06 175.69/60.06 [a__zeros()] = [0] 175.69/60.06 [0] 175.69/60.06 >= [0] 175.69/60.06 [0] 175.69/60.06 = [zeros()] 175.69/60.06 175.69/60.06 [a__tail(X)] = [1 0] X + [1] 175.69/60.06 [0 1] [1] 175.69/60.06 > [1 0] X + [0] 175.69/60.06 [0 1] [1] 175.69/60.06 = [tail(X)] 175.69/60.06 175.69/60.06 [a__tail(cons(X, XS))] = [1 0] X + [1 2] XS + [1] 175.69/60.06 [0 1] [0 1] [1] 175.69/60.06 > [1 1] XS + [0] 175.69/60.06 [0 1] [0] 175.69/60.06 = [mark(XS)] 175.69/60.06 175.69/60.06 [mark(cons(X1, X2))] = [1 1] X1 + [1 3] X2 + [0] 175.69/60.06 [0 1] [0 1] [0] 175.69/60.06 >= [1 1] X1 + [1 2] X2 + [0] 175.69/60.06 [0 1] [0 1] [0] 175.69/60.06 = [cons(mark(X1), X2)] 175.69/60.06 175.69/60.06 [mark(0())] = [0] 175.69/60.06 [0] 175.69/60.06 >= [0] 175.69/60.06 [0] 175.69/60.06 = [0()] 175.69/60.06 175.69/60.06 [mark(zeros())] = [0] 175.69/60.06 [0] 175.69/60.06 >= [0] 175.69/60.06 [0] 175.69/60.06 = [a__zeros()] 175.69/60.06 175.69/60.06 [mark(tail(X))] = [1 1] X + [1] 175.69/60.06 [0 1] [1] 175.69/60.06 >= [1 1] X + [1] 175.69/60.06 [0 1] [1] 175.69/60.06 = [a__tail(mark(X))] 175.69/60.06 175.69/60.06 175.69/60.06 We return to the main proof. 175.69/60.06 175.69/60.06 We are left with following problem, upon which TcT provides the 175.69/60.06 certificate YES(O(1),O(n^2)). 175.69/60.06 175.69/60.06 Strict Trs: { mark(cons(X1, X2)) -> cons(mark(X1), X2) } 175.69/60.06 Weak Trs: 175.69/60.06 { a__zeros() -> cons(0(), zeros()) 175.69/60.06 , a__zeros() -> zeros() 175.69/60.06 , a__tail(X) -> tail(X) 175.69/60.06 , a__tail(cons(X, XS)) -> mark(XS) 175.69/60.06 , mark(0()) -> 0() 175.69/60.06 , mark(zeros()) -> a__zeros() 175.69/60.06 , mark(tail(X)) -> a__tail(mark(X)) } 175.69/60.06 Obligation: 175.69/60.06 derivational complexity 175.69/60.06 Answer: 175.69/60.06 YES(O(1),O(n^2)) 175.69/60.06 175.69/60.06 We use the processor 'matrix interpretation of dimension 2' to 175.69/60.06 orient following rules strictly. 175.69/60.06 175.69/60.06 Trs: { mark(cons(X1, X2)) -> cons(mark(X1), X2) } 175.69/60.06 175.69/60.06 The induced complexity on above rules (modulo remaining rules) is 175.69/60.06 YES(?,O(n^2)) . These rules are moved into the corresponding weak 175.69/60.06 component(s). 175.69/60.06 175.69/60.06 Sub-proof: 175.69/60.06 ---------- 175.69/60.06 TcT has computed the following triangular matrix interpretation. 175.69/60.06 175.69/60.06 [a__zeros] = [0] 175.69/60.06 [1] 175.69/60.06 175.69/60.06 [cons](x1, x2) = [1 0] x1 + [1 2] x2 + [0] 175.69/60.06 [0 1] [0 1] [1] 175.69/60.06 175.69/60.06 [0] = [0] 175.69/60.06 [0] 175.69/60.06 175.69/60.06 [zeros] = [0] 175.69/60.06 [0] 175.69/60.06 175.69/60.06 [a__tail](x1) = [1 0] x1 + [0] 175.69/60.06 [0 1] [0] 175.69/60.06 175.69/60.06 [mark](x1) = [1 1] x1 + [0] 175.69/60.06 [0 1] [1] 175.69/60.06 175.69/60.06 [tail](x1) = [1 0] x1 + [0] 175.69/60.06 [0 1] [0] 175.69/60.06 175.69/60.06 The order satisfies the following ordering constraints: 175.69/60.06 175.69/60.06 [a__zeros()] = [0] 175.69/60.06 [1] 175.69/60.06 >= [0] 175.69/60.06 [1] 175.69/60.06 = [cons(0(), zeros())] 175.69/60.06 175.69/60.06 [a__zeros()] = [0] 175.69/60.06 [1] 175.69/60.06 >= [0] 175.69/60.06 [0] 175.69/60.06 = [zeros()] 175.69/60.06 175.69/60.06 [a__tail(X)] = [1 0] X + [0] 175.69/60.06 [0 1] [0] 175.69/60.06 >= [1 0] X + [0] 175.69/60.06 [0 1] [0] 175.69/60.06 = [tail(X)] 175.69/60.06 175.69/60.06 [a__tail(cons(X, XS))] = [1 0] X + [1 2] XS + [0] 175.69/60.06 [0 1] [0 1] [1] 175.69/60.06 >= [1 1] XS + [0] 175.69/60.06 [0 1] [1] 175.69/60.06 = [mark(XS)] 175.69/60.06 175.69/60.06 [mark(cons(X1, X2))] = [1 1] X1 + [1 3] X2 + [1] 175.69/60.06 [0 1] [0 1] [2] 175.69/60.06 > [1 1] X1 + [1 2] X2 + [0] 175.69/60.06 [0 1] [0 1] [2] 175.69/60.06 = [cons(mark(X1), X2)] 175.69/60.06 175.69/60.06 [mark(0())] = [0] 175.69/60.06 [1] 175.69/60.06 >= [0] 175.69/60.06 [0] 175.69/60.06 = [0()] 175.69/60.06 175.69/60.06 [mark(zeros())] = [0] 175.69/60.06 [1] 175.69/60.06 >= [0] 175.69/60.06 [1] 175.69/60.06 = [a__zeros()] 175.69/60.06 175.69/60.06 [mark(tail(X))] = [1 1] X + [0] 175.69/60.06 [0 1] [1] 175.69/60.06 >= [1 1] X + [0] 175.69/60.06 [0 1] [1] 175.69/60.06 = [a__tail(mark(X))] 175.69/60.06 175.69/60.06 175.69/60.06 We return to the main proof. 175.69/60.06 175.69/60.06 We are left with following problem, upon which TcT provides the 175.69/60.06 certificate YES(O(1),O(1)). 175.69/60.06 175.69/60.06 Weak Trs: 175.69/60.06 { a__zeros() -> cons(0(), zeros()) 175.69/60.06 , a__zeros() -> zeros() 175.69/60.06 , a__tail(X) -> tail(X) 175.69/60.06 , a__tail(cons(X, XS)) -> mark(XS) 175.69/60.06 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 175.69/60.06 , mark(0()) -> 0() 175.69/60.06 , mark(zeros()) -> a__zeros() 175.69/60.06 , mark(tail(X)) -> a__tail(mark(X)) } 175.69/60.06 Obligation: 175.69/60.06 derivational complexity 175.69/60.06 Answer: 175.69/60.06 YES(O(1),O(1)) 175.69/60.06 175.69/60.06 Empty rules are trivially bounded 175.69/60.06 175.69/60.06 Hurray, we answered YES(O(1),O(n^2)) 175.69/60.08 EOF