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