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