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