YES(O(1),O(n^2)) 987.86/297.11 YES(O(1),O(n^2)) 987.86/297.11 987.86/297.11 We are left with following problem, upon which TcT provides the 987.86/297.11 certificate YES(O(1),O(n^2)). 987.86/297.11 987.86/297.11 Strict Trs: 987.86/297.11 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.11 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.11 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.11 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.11 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.11 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.11 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.11 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.11 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.11 , 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 987.86/297.11 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.11 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.11 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.11 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.11 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.11 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.11 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.11 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.11 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.11 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.11 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.11 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.11 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.11 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.11 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.11 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.11 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.11 , 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 987.86/297.11 , 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 987.86/297.11 , 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 987.86/297.11 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.11 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.11 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.11 , 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.11 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.11 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 987.86/297.11 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 987.86/297.11 , 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.11 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.11 Obligation: 987.86/297.11 derivational complexity 987.86/297.11 Answer: 987.86/297.11 YES(O(1),O(n^2)) 987.86/297.11 987.86/297.11 We use the processor 'matrix interpretation of dimension 3' to 987.86/297.11 orient following rules strictly. 987.86/297.11 987.86/297.11 Trs: { 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) } 987.86/297.11 987.86/297.11 The induced complexity on above rules (modulo remaining rules) is 987.86/297.11 YES(?,O(n^1)) . These rules are moved into the corresponding weak 987.86/297.11 component(s). 987.86/297.11 987.86/297.11 Sub-proof: 987.86/297.11 ---------- 987.86/297.11 TcT has computed the following triangular matrix interpretation. 987.86/297.11 Note that the diagonal of the component-wise maxima of 987.86/297.11 interpretation-entries contains no more than 1 non-zero entries. 987.86/297.11 987.86/297.11 [1 0 0] [0] 987.86/297.11 [0](x1) = [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 987.86/297.11 [1 0 0] [0] 987.86/297.11 [1](x1) = [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 987.86/297.11 [1 0 0] [0] 987.86/297.11 [2](x1) = [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 987.86/297.11 [1 0 1] [0] 987.86/297.11 [3](x1) = [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 987.86/297.11 [1 0 0] [0] 987.86/297.11 [4](x1) = [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [2] 987.86/297.11 987.86/297.11 [1 0 0] [0] 987.86/297.11 [5](x1) = [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 987.86/297.11 The order satisfies the following ordering constraints: 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(0(2(2(1(2(x1))))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(1(2(0(x1))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(1(2(4(2(0(x1))))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(1(3(0(2(x1)))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(1(3(0(4(x1)))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(2(0(1(2(x1)))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(3(0(1(2(x1)))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(3(0(3(1(x1)))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(3(1(0(x1))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(4(0(4(1(x1)))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(0(4(0(x1))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(0(2(0(x1)))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(0(3(0(4(x1))))))] 987.86/297.11 987.86/297.11 [0(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(2(0(0(x1)))))] 987.86/297.11 987.86/297.11 [0(0(1(5(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(4(1(0(5(x1)))))] 987.86/297.11 987.86/297.11 [0(0(2(1(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [2(0(3(0(2(1(x1))))))] 987.86/297.11 987.86/297.11 [0(0(2(1(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [2(3(0(2(0(1(x1))))))] 987.86/297.11 987.86/297.11 [0(0(5(1(5(x1)))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(5(5(0(0(x1))))))] 987.86/297.11 987.86/297.11 [0(1(0(1(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(0(2(0(1(x1)))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(2(1(1(x1))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(3(1(1(x1))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(0(3(1(2(4(x1))))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(0(4(2(1(2(x1))))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(1(2(4(3(0(x1))))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(1(3(0(4(x1)))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(0(2(1(x1)))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(1(0(4(4(x1))))))] 987.86/297.11 987.86/297.11 [0(1(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(2(1(3(0(x1))))))] 987.86/297.11 987.86/297.11 [0(1(1(1(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(1(3(1(0(x1)))))] 987.86/297.11 987.86/297.11 [0(5(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(2(3(1(5(x1)))))] 987.86/297.11 987.86/297.11 [0(5(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(3(1(2(5(2(x1))))))] 987.86/297.11 987.86/297.11 [0(5(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(3(1(5(x1))))] 987.86/297.11 987.86/297.11 [0(5(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(3(1(5(2(x1)))))] 987.86/297.11 987.86/297.11 [0(5(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(4(5(1(x1))))] 987.86/297.11 987.86/297.11 [0(5(3(0(1(x1)))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(0(5(3(0(4(x1))))))] 987.86/297.11 987.86/297.11 [0(5(3(4(1(x1)))))] = [1 0 0] [2] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 > [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(0(3(5(4(5(x1))))))] 987.86/297.11 987.86/297.11 [0(5(4(0(1(x1)))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [0(1(3(0(4(5(x1))))))] 987.86/297.11 987.86/297.11 [5(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [5(0(2(1(2(4(x1))))))] 987.86/297.11 987.86/297.11 [5(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [5(1(2(3(0(4(x1))))))] 987.86/297.11 987.86/297.11 [5(0(1(x1)))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [5(1(2(4(0(x1)))))] 987.86/297.11 987.86/297.11 [5(0(1(1(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(5(1(2(0(x1)))))] 987.86/297.11 987.86/297.11 [5(3(0(1(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [5(1(2(3(0(x1)))))] 987.86/297.11 987.86/297.11 [5(3(1(5(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [5(3(1(2(5(x1)))))] 987.86/297.11 987.86/297.11 [5(3(2(1(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(3(5(2(x1)))))] 987.86/297.11 987.86/297.11 [5(4(0(1(x1))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [1(2(5(0(4(x1)))))] 987.86/297.11 987.86/297.11 [5(4(2(1(1(x1)))))] = [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 >= [1 0 0] [0] 987.86/297.11 [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.11 = [5(4(1(2(1(2(x1))))))] 987.86/297.11 987.86/297.11 987.86/297.11 We return to the main proof. 987.86/297.11 987.86/297.11 We are left with following problem, upon which TcT provides the 987.86/297.11 certificate YES(O(1),O(n^2)). 987.86/297.11 987.86/297.11 Strict Trs: 987.86/297.11 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.11 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.11 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.11 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.11 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.11 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.11 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.11 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.11 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.11 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.11 , 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 987.86/297.11 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.11 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.11 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.11 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.11 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.11 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.11 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.11 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.11 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.11 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.11 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.11 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.11 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.11 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.11 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.11 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.11 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.11 , 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 987.86/297.11 , 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 987.86/297.11 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.11 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.11 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.11 , 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.11 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.11 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 987.86/297.11 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 987.86/297.11 , 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.11 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.11 Weak Trs: { 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) } 987.86/297.11 Obligation: 987.86/297.11 derivational complexity 987.86/297.11 Answer: 987.86/297.11 YES(O(1),O(n^2)) 987.86/297.11 987.86/297.11 We use the processor 'matrix interpretation of dimension 3' to 987.86/297.11 orient following rules strictly. 987.86/297.11 987.86/297.11 Trs: { 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) } 987.86/297.11 987.86/297.11 The induced complexity on above rules (modulo remaining rules) is 987.86/297.11 YES(?,O(n^1)) . These rules are moved into the corresponding weak 987.86/297.11 component(s). 987.86/297.11 987.86/297.11 Sub-proof: 987.86/297.11 ---------- 987.86/297.11 TcT has computed the following triangular matrix interpretation. 987.86/297.11 Note that the diagonal of the component-wise maxima of 987.86/297.11 interpretation-entries contains no more than 1 non-zero entries. 987.86/297.11 987.86/297.11 [1 2 0] [0] 987.86/297.11 [0](x1) = [0 0 0] x1 + [0] 987.86/297.11 [0 0 0] [0] 987.86/297.12 987.86/297.12 [1 2 0] [0] 987.86/297.12 [1](x1) = [0 0 2] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 987.86/297.12 [1 2 0] [0] 987.86/297.12 [2](x1) = [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 987.86/297.12 [1 0 0] [0] 987.86/297.12 [3](x1) = [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 987.86/297.12 [1 0 0] [0] 987.86/297.12 [4](x1) = [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 987.86/297.12 [1 2 0] [0] 987.86/297.12 [5](x1) = [0 0 1] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 987.86/297.12 The order satisfies the following ordering constraints: 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(0(2(2(1(2(x1))))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(1(2(0(x1))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(1(2(4(2(0(x1))))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(1(3(0(2(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(1(3(0(4(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(2(0(1(2(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(3(0(1(2(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(3(0(3(1(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(3(1(0(x1))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(4(0(4(1(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(4(0(x1))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(0(2(0(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(0(3(0(4(x1))))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(2(0(0(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(5(x1))))] = [1 2 2] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 2] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(4(1(0(5(x1)))))] 987.86/297.12 987.86/297.12 [0(0(2(1(x1))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [2(0(3(0(2(1(x1))))))] 987.86/297.12 987.86/297.12 [0(0(2(1(x1))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [2(3(0(2(0(1(x1))))))] 987.86/297.12 987.86/297.12 [0(0(5(1(5(x1)))))] = [1 2 2] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(5(5(0(0(x1))))))] 987.86/297.12 987.86/297.12 [0(1(0(1(x1))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(2(0(1(x1)))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(2(1(1(x1))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(3(1(1(x1))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(3(1(2(4(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(4(2(1(2(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(1(2(4(3(0(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(1(3(0(4(x1)))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(0(2(1(x1)))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(1(0(4(4(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(2(1(3(0(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(1(x1))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(1(3(1(0(x1)))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 2] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(2(3(1(5(x1)))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(3(1(2(5(2(x1))))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 2] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(3(1(5(x1))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(3(1(5(2(x1)))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(4(5(1(x1))))] 987.86/297.12 987.86/297.12 [0(5(3(0(1(x1)))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(5(3(0(4(x1))))))] 987.86/297.12 987.86/297.12 [0(5(3(4(1(x1)))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(3(5(4(5(x1))))))] 987.86/297.12 987.86/297.12 [0(5(4(0(1(x1)))))] = [1 2 4] [4] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 > [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [0(1(3(0(4(5(x1))))))] 987.86/297.12 987.86/297.12 [5(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(0(2(1(2(4(x1))))))] 987.86/297.12 987.86/297.12 [5(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(1(2(3(0(4(x1))))))] 987.86/297.12 987.86/297.12 [5(0(1(x1)))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(1(2(4(0(x1)))))] 987.86/297.12 987.86/297.12 [5(0(1(1(x1))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(5(1(2(0(x1)))))] 987.86/297.12 987.86/297.12 [5(3(0(1(x1))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(1(2(3(0(x1)))))] 987.86/297.12 987.86/297.12 [5(3(1(5(x1))))] = [1 2 2] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 2] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(3(1(2(5(x1)))))] 987.86/297.12 987.86/297.12 [5(3(2(1(x1))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(3(5(2(x1)))))] 987.86/297.12 987.86/297.12 [5(4(0(1(x1))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [2] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(5(0(4(x1)))))] 987.86/297.12 987.86/297.12 [5(4(2(1(1(x1)))))] = [1 2 4] [0] 987.86/297.12 [0 0 0] x1 + [2] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [2] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(4(1(2(1(2(x1))))))] 987.86/297.12 987.86/297.12 987.86/297.12 We return to the main proof. 987.86/297.12 987.86/297.12 We are left with following problem, upon which TcT provides the 987.86/297.12 certificate YES(O(1),O(n^2)). 987.86/297.12 987.86/297.12 Strict Trs: 987.86/297.12 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.12 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.12 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.12 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.12 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.12 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.12 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.12 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.12 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.12 , 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 987.86/297.12 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.12 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.12 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.12 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.12 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.12 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.12 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.12 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.12 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.12 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.12 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.12 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.12 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.12 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.12 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.12 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.12 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.12 , 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 987.86/297.12 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.12 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.12 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.12 , 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.12 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.12 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 987.86/297.12 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 987.86/297.12 , 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.12 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.12 Weak Trs: 987.86/297.12 { 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 987.86/297.12 , 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) } 987.86/297.12 Obligation: 987.86/297.12 derivational complexity 987.86/297.12 Answer: 987.86/297.12 YES(O(1),O(n^2)) 987.86/297.12 987.86/297.12 We use the processor 'matrix interpretation of dimension 3' to 987.86/297.12 orient following rules strictly. 987.86/297.12 987.86/297.12 Trs: 987.86/297.12 { 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.12 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.12 987.86/297.12 The induced complexity on above rules (modulo remaining rules) is 987.86/297.12 YES(?,O(n^1)) . These rules are moved into the corresponding weak 987.86/297.12 component(s). 987.86/297.12 987.86/297.12 Sub-proof: 987.86/297.12 ---------- 987.86/297.12 TcT has computed the following triangular matrix interpretation. 987.86/297.12 Note that the diagonal of the component-wise maxima of 987.86/297.12 interpretation-entries contains no more than 1 non-zero entries. 987.86/297.12 987.86/297.12 [1 0 0] [0] 987.86/297.12 [0](x1) = [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 987.86/297.12 [1 2 0] [0] 987.86/297.12 [1](x1) = [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 987.86/297.12 [1 0 0] [0] 987.86/297.12 [2](x1) = [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 987.86/297.12 [1 0 0] [0] 987.86/297.12 [3](x1) = [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 987.86/297.12 [1 0 0] [0] 987.86/297.12 [4](x1) = [0 0 1] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 987.86/297.12 [1 2 0] [0] 987.86/297.12 [5](x1) = [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 987.86/297.12 The order satisfies the following ordering constraints: 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(0(2(2(1(2(x1))))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(1(2(0(x1))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(1(2(4(2(0(x1))))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(1(3(0(2(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(1(3(0(4(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(2(0(1(2(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(3(0(1(2(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(3(0(3(1(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(3(1(0(x1))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(4(0(4(1(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(4(0(x1))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(0(2(0(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(0(3(0(4(x1))))))] 987.86/297.12 987.86/297.12 [0(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(2(0(0(x1)))))] 987.86/297.12 987.86/297.12 [0(0(1(5(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(4(1(0(5(x1)))))] 987.86/297.12 987.86/297.12 [0(0(2(1(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [2(0(3(0(2(1(x1))))))] 987.86/297.12 987.86/297.12 [0(0(2(1(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [2(3(0(2(0(1(x1))))))] 987.86/297.12 987.86/297.12 [0(0(5(1(5(x1)))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(5(5(0(0(x1))))))] 987.86/297.12 987.86/297.12 [0(1(0(1(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(2(0(1(x1)))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(2(1(1(x1))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(3(1(1(x1))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(3(1(2(4(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(4(2(1(2(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(1(2(4(3(0(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(1(3(0(4(x1)))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(0(2(1(x1)))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(1(0(4(4(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(2(1(3(0(x1))))))] 987.86/297.12 987.86/297.12 [0(1(1(1(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(1(3(1(0(x1)))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(2(3(1(5(x1)))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(3(1(2(5(2(x1))))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(3(1(5(x1))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(3(1(5(2(x1)))))] 987.86/297.12 987.86/297.12 [0(5(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(4(5(1(x1))))] 987.86/297.12 987.86/297.12 [0(5(3(0(1(x1)))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(5(3(0(4(x1))))))] 987.86/297.12 987.86/297.12 [0(5(3(4(1(x1)))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(0(3(5(4(5(x1))))))] 987.86/297.12 987.86/297.12 [0(5(4(0(1(x1)))))] = [1 2 0] [4] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 > [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [2] 987.86/297.12 = [0(1(3(0(4(5(x1))))))] 987.86/297.12 987.86/297.12 [5(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(0(2(1(2(4(x1))))))] 987.86/297.12 987.86/297.12 [5(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(1(2(3(0(4(x1))))))] 987.86/297.12 987.86/297.12 [5(0(1(x1)))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(1(2(4(0(x1)))))] 987.86/297.12 987.86/297.12 [5(0(1(1(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(5(1(2(0(x1)))))] 987.86/297.12 987.86/297.12 [5(3(0(1(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(1(2(3(0(x1)))))] 987.86/297.12 987.86/297.12 [5(3(1(5(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(3(1(2(5(x1)))))] 987.86/297.12 987.86/297.12 [5(3(2(1(x1))))] = [1 2 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 >= [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(3(5(2(x1)))))] 987.86/297.12 987.86/297.12 [5(4(0(1(x1))))] = [1 2 0] [4] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 > [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [1(2(5(0(4(x1)))))] 987.86/297.12 987.86/297.12 [5(4(2(1(1(x1)))))] = [1 2 0] [4] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 > [1 0 0] [0] 987.86/297.12 [0 0 0] x1 + [0] 987.86/297.12 [0 0 0] [0] 987.86/297.12 = [5(4(1(2(1(2(x1))))))] 987.86/297.12 987.86/297.12 987.86/297.12 We return to the main proof. 987.86/297.12 987.86/297.12 We are left with following problem, upon which TcT provides the 987.86/297.12 certificate YES(O(1),O(n^2)). 987.86/297.12 987.86/297.12 Strict Trs: 987.86/297.12 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.12 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.12 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.12 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.12 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.12 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.12 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.12 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.12 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.13 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.13 , 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 987.86/297.13 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.13 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.13 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.13 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.13 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.13 , 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 987.86/297.13 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.13 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.13 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.13 , 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.13 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.13 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 987.86/297.13 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) } 987.86/297.13 Weak Trs: 987.86/297.13 { 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 987.86/297.13 , 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 987.86/297.13 , 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.13 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.13 Obligation: 987.86/297.13 derivational complexity 987.86/297.13 Answer: 987.86/297.13 YES(O(1),O(n^2)) 987.86/297.13 987.86/297.13 We use the processor 'matrix interpretation of dimension 3' to 987.86/297.13 orient following rules strictly. 987.86/297.13 987.86/297.13 Trs: 987.86/297.13 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.13 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.13 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.13 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.13 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.13 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.13 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.13 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.13 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.13 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.13 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.13 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.13 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.13 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.13 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.13 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.13 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.13 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) } 987.86/297.13 987.86/297.13 The induced complexity on above rules (modulo remaining rules) is 987.86/297.13 YES(?,O(n^1)) . These rules are moved into the corresponding weak 987.86/297.13 component(s). 987.86/297.13 987.86/297.13 Sub-proof: 987.86/297.13 ---------- 987.86/297.13 TcT has computed the following triangular matrix interpretation. 987.86/297.13 Note that the diagonal of the component-wise maxima of 987.86/297.13 interpretation-entries contains no more than 1 non-zero entries. 987.86/297.13 987.86/297.13 [1 0 1] [0] 987.86/297.13 [0](x1) = [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 987.86/297.13 [1 0 1] [0] 987.86/297.13 [1](x1) = [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 987.86/297.13 [1 0 0] [0] 987.86/297.13 [2](x1) = [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 [1 0 0] [0] 987.86/297.13 [3](x1) = [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 [1 0 0] [0] 987.86/297.13 [4](x1) = [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 [1 0 1] [0] 987.86/297.13 [5](x1) = [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 987.86/297.13 The order satisfies the following ordering constraints: 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(0(2(2(1(2(x1))))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(1(2(0(x1))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(1(2(4(2(0(x1))))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(1(3(0(2(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(1(3(0(4(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(2(0(1(2(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(3(0(1(2(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(3(0(3(1(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(3(1(0(x1))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(4(0(4(1(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(0(4(0(x1))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(0(2(0(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(0(3(0(4(x1))))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(2(0(0(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(5(x1))))] = [1 0 1] [4] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(4(1(0(5(x1)))))] 987.86/297.13 987.86/297.13 [0(0(2(1(x1))))] = [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [2(0(3(0(2(1(x1))))))] 987.86/297.13 987.86/297.13 [0(0(2(1(x1))))] = [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 >= [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [2(3(0(2(0(1(x1))))))] 987.86/297.13 987.86/297.13 [0(0(5(1(5(x1)))))] = [1 0 1] [6] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [4] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(5(5(0(0(x1))))))] 987.86/297.13 987.86/297.13 [0(1(0(1(x1))))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(0(2(0(1(x1)))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(2(1(1(x1))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(3(1(1(x1))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(0(3(1(2(4(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(0(4(2(1(2(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(1(2(4(3(0(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(1(3(0(4(x1)))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(0(2(1(x1)))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(1(0(4(4(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(2(1(3(0(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(1(x1))))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(1(3(1(0(x1)))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(2(3(1(5(x1)))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(3(1(2(5(2(x1))))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(3(1(5(x1))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 0] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(3(1(5(2(x1)))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(4(5(1(x1))))] 987.86/297.13 987.86/297.13 [0(5(3(0(1(x1)))))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 >= [1 0 0] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(0(5(3(0(4(x1))))))] 987.86/297.13 987.86/297.13 [0(5(3(4(1(x1)))))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(0(3(5(4(5(x1))))))] 987.86/297.13 987.86/297.13 [0(5(4(0(1(x1)))))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [0(1(3(0(4(5(x1))))))] 987.86/297.13 987.86/297.13 [5(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 = [5(0(2(1(2(4(x1))))))] 987.86/297.13 987.86/297.13 [5(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 = [5(1(2(3(0(4(x1))))))] 987.86/297.13 987.86/297.13 [5(0(1(x1)))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 > [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 = [5(1(2(4(0(x1)))))] 987.86/297.13 987.86/297.13 [5(0(1(1(x1))))] = [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 >= [1 0 1] [3] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(5(1(2(0(x1)))))] 987.86/297.13 987.86/297.13 [5(3(0(1(x1))))] = [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 >= [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 = [5(1(2(3(0(x1)))))] 987.86/297.13 987.86/297.13 [5(3(1(5(x1))))] = [1 0 1] [2] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 > [1 0 1] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 = [5(3(1(2(5(x1)))))] 987.86/297.13 987.86/297.13 [5(3(2(1(x1))))] = [1 0 1] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 >= [1 0 0] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(3(5(2(x1)))))] 987.86/297.13 987.86/297.13 [5(4(0(1(x1))))] = [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 >= [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [1] 987.86/297.13 = [1(2(5(0(4(x1)))))] 987.86/297.13 987.86/297.13 [5(4(2(1(1(x1)))))] = [1 0 1] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 > [1 0 0] [0] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [2] 987.86/297.13 = [5(4(1(2(1(2(x1))))))] 987.86/297.13 987.86/297.13 987.86/297.13 We return to the main proof. 987.86/297.13 987.86/297.13 We are left with following problem, upon which TcT provides the 987.86/297.13 certificate YES(O(1),O(n^2)). 987.86/297.13 987.86/297.13 Strict Trs: 987.86/297.13 { 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 987.86/297.13 , 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 987.86/297.13 , 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.13 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.13 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) } 987.86/297.13 Weak Trs: 987.86/297.13 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.13 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.13 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.13 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.13 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.13 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.13 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.13 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.13 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.13 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.13 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.13 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.13 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.13 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.13 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.13 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.13 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.13 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.13 , 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 987.86/297.13 , 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 987.86/297.13 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.13 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.13 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.13 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 987.86/297.13 , 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.13 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.13 Obligation: 987.86/297.13 derivational complexity 987.86/297.13 Answer: 987.86/297.13 YES(O(1),O(n^2)) 987.86/297.13 987.86/297.13 We use the processor 'matrix interpretation of dimension 3' to 987.86/297.13 orient following rules strictly. 987.86/297.13 987.86/297.13 Trs: 987.86/297.13 { 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.13 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.13 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) } 987.86/297.13 987.86/297.13 The induced complexity on above rules (modulo remaining rules) is 987.86/297.13 YES(?,O(n^1)) . These rules are moved into the corresponding weak 987.86/297.13 component(s). 987.86/297.13 987.86/297.13 Sub-proof: 987.86/297.13 ---------- 987.86/297.13 TcT has computed the following triangular matrix interpretation. 987.86/297.13 Note that the diagonal of the component-wise maxima of 987.86/297.13 interpretation-entries contains no more than 1 non-zero entries. 987.86/297.13 987.86/297.13 [1 1 0] [0] 987.86/297.13 [0](x1) = [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 [1 1 0] [0] 987.86/297.13 [1](x1) = [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 [1 0 0] [0] 987.86/297.13 [2](x1) = [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 [1 0 0] [0] 987.86/297.13 [3](x1) = [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 [1 0 0] [0] 987.86/297.13 [4](x1) = [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 [1 1 0] [0] 987.86/297.13 [5](x1) = [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 987.86/297.13 The order satisfies the following ordering constraints: 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(0(2(2(1(2(x1))))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(1(2(0(x1))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(1(2(4(2(0(x1))))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 0 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(1(3(0(2(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 0 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(1(3(0(4(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(2(0(1(2(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 0 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(3(0(1(2(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(3(0(3(1(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(3(1(0(x1))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [0] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(4(0(4(1(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(0(4(0(x1))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [0] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(2(0(2(0(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(2(0(3(0(4(x1))))))] 987.86/297.13 987.86/297.13 [0(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(2(2(0(0(x1)))))] 987.86/297.13 987.86/297.13 [0(0(1(5(x1))))] = [1 1 0] [3] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(4(1(0(5(x1)))))] 987.86/297.13 987.86/297.13 [0(0(2(1(x1))))] = [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [2(0(3(0(2(1(x1))))))] 987.86/297.13 987.86/297.13 [0(0(2(1(x1))))] = [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [0] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [2(3(0(2(0(1(x1))))))] 987.86/297.13 987.86/297.13 [0(0(5(1(5(x1)))))] = [1 1 0] [4] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [3] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(2(5(5(0(0(x1))))))] 987.86/297.13 987.86/297.13 [0(1(0(1(x1))))] = [1 1 0] [3] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(0(2(0(1(x1)))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(2(1(1(x1))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(3(1(1(x1))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 0 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(0(3(1(2(4(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(0(4(2(1(2(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(1(2(4(3(0(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 0 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(1(3(0(4(x1)))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [0] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(2(0(2(1(x1)))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(2(1(0(4(4(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(2(2(1(3(0(x1))))))] 987.86/297.13 987.86/297.13 [0(1(1(1(x1))))] = [1 1 0] [3] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [3] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(1(3(1(0(x1)))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(2(3(1(5(x1)))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(3(1(2(5(2(x1))))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(3(1(5(x1))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 0 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(3(1(5(2(x1)))))] 987.86/297.13 987.86/297.13 [0(5(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 1 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(4(5(1(x1))))] 987.86/297.13 987.86/297.13 [0(5(3(0(1(x1)))))] = [1 1 0] [3] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 0 0] [3] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(0(5(3(0(4(x1))))))] 987.86/297.13 987.86/297.13 [0(5(3(4(1(x1)))))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [1(0(3(5(4(5(x1))))))] 987.86/297.13 987.86/297.13 [0(5(4(0(1(x1)))))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 >= [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [0(1(3(0(4(5(x1))))))] 987.86/297.13 987.86/297.13 [5(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [5(0(2(1(2(4(x1))))))] 987.86/297.13 987.86/297.13 [5(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 > [1 0 0] [1] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.13 = [5(1(2(3(0(4(x1))))))] 987.86/297.13 987.86/297.13 [5(0(1(x1)))] = [1 1 0] [2] 987.86/297.13 [0 0 0] x1 + [1] 987.86/297.13 [0 0 0] [0] 987.86/297.14 > [1 1 0] [1] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 = [5(1(2(4(0(x1)))))] 987.86/297.14 987.86/297.14 [5(0(1(1(x1))))] = [1 1 0] [3] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 > [1 1 0] [2] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 = [1(5(1(2(0(x1)))))] 987.86/297.14 987.86/297.14 [5(3(0(1(x1))))] = [1 1 0] [2] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 > [1 1 0] [1] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 = [5(1(2(3(0(x1)))))] 987.86/297.14 987.86/297.14 [5(3(1(5(x1))))] = [1 1 0] [2] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 > [1 1 0] [1] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 = [5(3(1(2(5(x1)))))] 987.86/297.14 987.86/297.14 [5(3(2(1(x1))))] = [1 1 0] [1] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 > [1 0 0] [0] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 = [1(2(3(5(2(x1)))))] 987.86/297.14 987.86/297.14 [5(4(0(1(x1))))] = [1 1 0] [1] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 >= [1 0 0] [1] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 = [1(2(5(0(4(x1)))))] 987.86/297.14 987.86/297.14 [5(4(2(1(1(x1)))))] = [1 1 0] [1] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 > [1 0 0] [0] 987.86/297.14 [0 0 0] x1 + [1] 987.86/297.14 [0 0 0] [0] 987.86/297.14 = [5(4(1(2(1(2(x1))))))] 987.86/297.14 987.86/297.14 987.86/297.14 We return to the main proof. 987.86/297.14 987.86/297.14 We are left with following problem, upon which TcT provides the 987.86/297.14 certificate YES(O(1),O(n^2)). 987.86/297.14 987.86/297.14 Strict Trs: 987.86/297.14 { 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 987.86/297.14 , 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) } 987.86/297.14 Weak Trs: 987.86/297.14 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.14 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.14 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.14 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.14 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.14 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.14 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.14 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.14 , 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 987.86/297.14 , 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.14 , 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.14 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.14 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 987.86/297.14 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 987.86/297.14 , 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.14 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.14 Obligation: 987.86/297.14 derivational complexity 987.86/297.14 Answer: 987.86/297.14 YES(O(1),O(n^2)) 987.86/297.14 987.86/297.14 We use the processor 'matrix interpretation of dimension 2' to 987.86/297.14 orient following rules strictly. 987.86/297.14 987.86/297.14 Trs: { 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) } 987.86/297.14 987.86/297.14 The induced complexity on above rules (modulo remaining rules) is 987.86/297.14 YES(?,O(n^2)) . These rules are moved into the corresponding weak 987.86/297.14 component(s). 987.86/297.14 987.86/297.14 Sub-proof: 987.86/297.14 ---------- 987.86/297.14 TcT has computed the following triangular matrix interpretation. 987.86/297.14 987.86/297.14 [0](x1) = [1 2] x1 + [0] 987.86/297.14 [0 1] [0] 987.86/297.14 987.86/297.14 [1](x1) = [1 0] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 987.86/297.14 [2](x1) = [1 0] x1 + [0] 987.86/297.14 [0 1] [0] 987.86/297.14 987.86/297.14 [3](x1) = [1 0] x1 + [0] 987.86/297.14 [0 1] [0] 987.86/297.14 987.86/297.14 [4](x1) = [1 0] x1 + [0] 987.86/297.14 [0 1] [0] 987.86/297.14 987.86/297.14 [5](x1) = [1 0] x1 + [0] 987.86/297.14 [0 1] [0] 987.86/297.14 987.86/297.14 The order satisfies the following ordering constraints: 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(0(2(2(1(2(x1))))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(1(2(0(x1))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(1(2(4(2(0(x1))))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(1(3(0(2(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(1(3(0(4(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(2(0(1(2(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(3(0(1(2(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(3(0(3(1(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(3(1(0(x1))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(4(0(4(1(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(0(4(0(x1))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(2(0(2(0(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(2(0(3(0(4(x1))))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(2(2(0(0(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(5(x1))))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(4(1(0(5(x1)))))] 987.86/297.14 987.86/297.14 [0(0(2(1(x1))))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 = [2(0(3(0(2(1(x1))))))] 987.86/297.14 987.86/297.14 [0(0(2(1(x1))))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 = [2(3(0(2(0(1(x1))))))] 987.86/297.14 987.86/297.14 [0(0(5(1(5(x1)))))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(2(5(5(0(0(x1))))))] 987.86/297.14 987.86/297.14 [0(1(0(1(x1))))] = [1 4] x1 + [6] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 4] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(0(2(0(1(x1)))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 >= [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 = [0(2(1(1(x1))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 >= [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 = [0(3(1(1(x1))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 2] x1 + [2] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(0(3(1(2(4(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 2] x1 + [2] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(0(4(2(1(2(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(1(2(4(3(0(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(1(3(0(4(x1)))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 2] x1 + [2] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(2(0(2(1(x1)))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(2(1(0(4(4(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(2(2(1(3(0(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(1(x1))))] = [1 2] x1 + [6] 987.86/297.14 [0 1] [3] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [3] 987.86/297.14 = [1(1(3(1(0(x1)))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(2(3(1(5(x1)))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(3(1(2(5(2(x1))))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(3(1(5(x1))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(3(1(5(2(x1)))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(4(5(1(x1))))] 987.86/297.14 987.86/297.14 [0(5(3(0(1(x1)))))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(0(5(3(0(4(x1))))))] 987.86/297.14 987.86/297.14 [0(5(3(4(1(x1)))))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(0(3(5(4(5(x1))))))] 987.86/297.14 987.86/297.14 [0(5(4(0(1(x1)))))] = [1 4] x1 + [4] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 4] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [0(1(3(0(4(5(x1))))))] 987.86/297.14 987.86/297.14 [5(0(1(x1)))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 = [5(0(2(1(2(4(x1))))))] 987.86/297.14 987.86/297.14 [5(0(1(x1)))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [5(1(2(3(0(4(x1))))))] 987.86/297.14 987.86/297.14 [5(0(1(x1)))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [5(1(2(4(0(x1)))))] 987.86/297.14 987.86/297.14 [5(0(1(1(x1))))] = [1 2] x1 + [4] 987.86/297.14 [0 1] [2] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [2] 987.86/297.14 = [1(5(1(2(0(x1)))))] 987.86/297.14 987.86/297.14 [5(3(0(1(x1))))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [5(1(2(3(0(x1)))))] 987.86/297.14 987.86/297.14 [5(3(1(5(x1))))] = [1 0] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 0] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [5(3(1(2(5(x1)))))] 987.86/297.14 987.86/297.14 [5(3(2(1(x1))))] = [1 0] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 >= [1 0] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(2(3(5(2(x1)))))] 987.86/297.14 987.86/297.14 [5(4(0(1(x1))))] = [1 2] x1 + [2] 987.86/297.14 [0 1] [1] 987.86/297.14 > [1 2] x1 + [0] 987.86/297.14 [0 1] [1] 987.86/297.14 = [1(2(5(0(4(x1)))))] 987.86/297.14 987.86/297.14 [5(4(2(1(1(x1)))))] = [1 0] x1 + [0] 987.86/297.14 [0 1] [2] 987.86/297.14 >= [1 0] x1 + [0] 987.86/297.14 [0 1] [2] 987.86/297.14 = [5(4(1(2(1(2(x1))))))] 987.86/297.14 987.86/297.14 987.86/297.14 We return to the main proof. 987.86/297.14 987.86/297.14 We are left with following problem, upon which TcT provides the 987.86/297.14 certificate YES(O(1),O(n^2)). 987.86/297.14 987.86/297.14 Strict Trs: { 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) } 987.86/297.14 Weak Trs: 987.86/297.14 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.14 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.14 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.14 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.14 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.14 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.14 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.14 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.14 , 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 987.86/297.14 , 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 987.86/297.14 , 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.14 , 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.14 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.14 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 987.86/297.14 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 987.86/297.14 , 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.14 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.14 Obligation: 987.86/297.14 derivational complexity 987.86/297.14 Answer: 987.86/297.14 YES(O(1),O(n^2)) 987.86/297.14 987.86/297.14 We use the processor 'matrix interpretation of dimension 3' to 987.86/297.14 orient following rules strictly. 987.86/297.14 987.86/297.14 Trs: { 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) } 987.86/297.14 987.86/297.14 The induced complexity on above rules (modulo remaining rules) is 987.86/297.14 YES(?,O(n^2)) . These rules are moved into the corresponding weak 987.86/297.14 component(s). 987.86/297.14 987.86/297.14 Sub-proof: 987.86/297.14 ---------- 987.86/297.14 TcT has computed the following triangular matrix interpretation. 987.86/297.14 987.86/297.14 [1 1 0] [0] 987.86/297.14 [0](x1) = [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [0] 987.86/297.14 987.86/297.14 [1 1 0] [0] 987.86/297.14 [1](x1) = [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 987.86/297.14 [1 0 0] [0] 987.86/297.14 [2](x1) = [0 0 0] x1 + [0] 987.86/297.14 [0 0 1] [0] 987.86/297.14 987.86/297.14 [1 0 0] [0] 987.86/297.14 [3](x1) = [0 0 0] x1 + [0] 987.86/297.14 [0 0 1] [0] 987.86/297.14 987.86/297.14 [1 0 0] [0] 987.86/297.14 [4](x1) = [0 0 0] x1 + [0] 987.86/297.14 [0 0 1] [0] 987.86/297.14 987.86/297.14 [1 1 0] [0] 987.86/297.14 [5](x1) = [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [0] 987.86/297.14 987.86/297.14 The order satisfies the following ordering constraints: 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 >= [1 0 1] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(0(2(2(1(2(x1))))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(1(2(0(x1))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(1(2(4(2(0(x1))))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(1(3(0(2(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(1(3(0(4(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(2(0(1(2(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(3(0(1(2(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 0] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(3(0(3(1(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(3(1(0(x1))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 0] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(4(0(4(1(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(0(4(0(x1))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 0] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(2(0(2(0(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 0] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(2(0(3(0(4(x1))))))] 987.86/297.14 987.86/297.14 [0(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(2(2(0(0(x1)))))] 987.86/297.14 987.86/297.14 [0(0(1(5(x1))))] = [1 1 3] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 2] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(4(1(0(5(x1)))))] 987.86/297.14 987.86/297.14 [0(0(2(1(x1))))] = [1 1 1] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 0] [0] 987.86/297.14 [0 0 0] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [2(0(3(0(2(1(x1))))))] 987.86/297.14 987.86/297.14 [0(0(2(1(x1))))] = [1 1 1] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 0] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [2(3(0(2(0(1(x1))))))] 987.86/297.14 987.86/297.14 [0(0(5(1(5(x1)))))] = [1 1 4] [2] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 3] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(2(5(5(0(0(x1))))))] 987.86/297.14 987.86/297.14 [0(1(0(1(x1))))] = [1 1 3] [2] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(0(2(0(1(x1)))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [0(2(1(1(x1))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [0(3(1(1(x1))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 >= [1 0 1] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(0(3(1(2(4(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 >= [1 0 1] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(0(4(2(1(2(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(1(2(4(3(0(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(1(3(0(4(x1)))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 1 0] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(2(0(2(1(x1)))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(2(1(0(4(4(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 1 0] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(2(2(1(3(0(x1))))))] 987.86/297.14 987.86/297.14 [0(1(1(1(x1))))] = [1 1 3] [3] 987.86/297.14 [0 0 1] x1 + [3] 987.86/297.14 [0 0 1] [3] 987.86/297.14 > [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [3] 987.86/297.14 = [1(1(3(1(0(x1)))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(2(3(1(5(x1)))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 0] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(3(1(2(5(2(x1))))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(3(1(5(x1))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(3(1(5(2(x1)))))] 987.86/297.14 987.86/297.14 [0(5(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(4(5(1(x1))))] 987.86/297.14 987.86/297.14 [0(5(3(0(1(x1)))))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 2] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(0(5(3(0(4(x1))))))] 987.86/297.14 987.86/297.14 [0(5(3(4(1(x1)))))] = [1 1 1] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(0(3(5(4(5(x1))))))] 987.86/297.14 987.86/297.14 [0(5(4(0(1(x1)))))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [0(1(3(0(4(5(x1))))))] 987.86/297.14 987.86/297.14 [5(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 >= [1 0 1] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [5(0(2(1(2(4(x1))))))] 987.86/297.14 987.86/297.14 [5(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [5(1(2(3(0(4(x1))))))] 987.86/297.14 987.86/297.14 [5(0(1(x1)))] = [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 > [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [5(1(2(4(0(x1)))))] 987.86/297.14 987.86/297.14 [5(0(1(1(x1))))] = [1 1 3] [3] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 > [1 1 2] [1] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [1(5(1(2(0(x1)))))] 987.86/297.14 987.86/297.14 [5(3(0(1(x1))))] = [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 >= [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [5(1(2(3(0(x1)))))] 987.86/297.14 987.86/297.14 [5(3(1(5(x1))))] = [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 >= [1 1 0] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [5(3(1(2(5(x1)))))] 987.86/297.14 987.86/297.14 [5(3(2(1(x1))))] = [1 1 0] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 >= [1 0 0] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(2(3(5(2(x1)))))] 987.86/297.14 987.86/297.14 [5(4(0(1(x1))))] = [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [1] 987.86/297.14 [0 0 1] [1] 987.86/297.14 >= [1 0 1] [0] 987.86/297.14 [0 0 1] x1 + [0] 987.86/297.14 [0 0 1] [1] 987.86/297.14 = [1(2(5(0(4(x1)))))] 987.86/297.14 987.86/297.14 [5(4(2(1(1(x1)))))] = [1 1 1] [0] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 >= [1 0 0] [0] 987.86/297.14 [0 0 1] x1 + [2] 987.86/297.14 [0 0 1] [2] 987.86/297.14 = [5(4(1(2(1(2(x1))))))] 987.86/297.14 987.86/297.14 987.86/297.14 We return to the main proof. 987.86/297.14 987.86/297.14 We are left with following problem, upon which TcT provides the 987.86/297.14 certificate YES(O(1),O(1)). 987.86/297.14 987.86/297.14 Weak Trs: 987.86/297.14 { 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(2(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 0(3(1(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 1(0(4(0(x1)))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 987.86/297.14 , 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 987.86/297.14 , 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 987.86/297.14 , 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 987.86/297.14 , 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 987.86/297.14 , 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 987.86/297.14 , 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 0(2(1(1(x1)))) 987.86/297.14 , 0(1(1(x1))) -> 0(3(1(1(x1)))) 987.86/297.14 , 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 987.86/297.14 , 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 987.86/297.14 , 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(5(x1)))) 987.86/297.14 , 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 987.86/297.14 , 0(5(1(x1))) -> 0(4(5(1(x1)))) 987.86/297.14 , 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 987.86/297.14 , 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 987.86/297.14 , 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 987.86/297.14 , 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 987.86/297.14 , 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 987.86/297.14 , 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 987.86/297.14 , 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 987.86/297.14 , 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 987.86/297.14 , 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 987.86/297.14 , 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) } 987.86/297.14 Obligation: 987.86/297.14 derivational complexity 987.86/297.14 Answer: 987.86/297.14 YES(O(1),O(1)) 987.86/297.14 987.86/297.14 Empty rules are trivially bounded 987.86/297.14 987.86/297.14 Hurray, we answered YES(O(1),O(n^2)) 988.01/297.25 EOF