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