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