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