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