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