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