YES(O(1),O(n^1)) 808.21/298.46 YES(O(1),O(n^1)) 808.21/298.46 808.21/298.46 We are left with following problem, upon which TcT provides the 808.21/298.46 certificate YES(O(1),O(n^1)). 808.21/298.46 808.21/298.46 Strict Trs: 808.21/298.46 { +(x, 0()) -> x 808.21/298.46 , +(x, i(x)) -> 0() 808.21/298.46 , +(+(x, y), z) -> +(x, +(y, z)) 808.21/298.46 , *(x, +(y, z)) -> +(*(x, y), *(x, z)) 808.21/298.46 , *(+(x, y), z) -> +(*(x, z), *(y, z)) } 808.21/298.46 Obligation: 808.21/298.46 runtime complexity 808.21/298.46 Answer: 808.21/298.46 YES(O(1),O(n^1)) 808.21/298.46 808.21/298.46 The weightgap principle applies (using the following nonconstant 808.21/298.46 growth matrix-interpretation) 808.21/298.46 808.21/298.46 The following argument positions are usable: 808.21/298.46 Uargs(+) = {1, 2} 808.21/298.46 808.21/298.46 TcT has computed the following matrix interpretation satisfying 808.21/298.46 not(EDA) and not(IDA(1)). 808.21/298.46 808.21/298.46 [+](x1, x2) = [1] x1 + [1] x2 + [7] 808.21/298.46 808.21/298.46 [0] = [7] 808.21/298.46 808.21/298.46 [i](x1) = [1] x1 + [7] 808.21/298.46 808.21/298.46 [*](x1, x2) = [3] 808.21/298.46 808.21/298.46 The order satisfies the following ordering constraints: 808.21/298.46 808.21/298.46 [+(x, 0())] = [1] x + [14] 808.21/298.46 > [1] x + [0] 808.21/298.46 = [x] 808.21/298.46 808.21/298.46 [+(x, i(x))] = [2] x + [14] 808.21/298.46 > [7] 808.21/298.46 = [0()] 808.21/298.46 808.21/298.46 [+(+(x, y), z)] = [1] x + [1] y + [1] z + [14] 808.21/298.46 >= [1] x + [1] y + [1] z + [14] 808.21/298.46 = [+(x, +(y, z))] 808.21/298.46 808.21/298.46 [*(x, +(y, z))] = [3] 808.21/298.46 ? [13] 808.21/298.46 = [+(*(x, y), *(x, z))] 808.21/298.46 808.21/298.46 [*(+(x, y), z)] = [3] 808.21/298.46 ? [13] 808.21/298.46 = [+(*(x, z), *(y, z))] 808.21/298.46 808.21/298.46 808.21/298.46 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 808.21/298.46 808.21/298.46 We are left with following problem, upon which TcT provides the 808.21/298.46 certificate YES(O(1),O(1)). 808.21/298.46 808.21/298.46 Strict Trs: 808.21/298.46 { +(+(x, y), z) -> +(x, +(y, z)) 808.21/298.46 , *(x, +(y, z)) -> +(*(x, y), *(x, z)) 808.21/298.46 , *(+(x, y), z) -> +(*(x, z), *(y, z)) } 808.21/298.46 Weak Trs: 808.21/298.46 { +(x, 0()) -> x 808.21/298.46 , +(x, i(x)) -> 0() } 808.21/298.46 Obligation: 808.21/298.46 runtime complexity 808.21/298.46 Answer: 808.21/298.46 YES(O(1),O(1)) 808.21/298.46 808.21/298.46 We use the processor 'polynomial interpretation' to orient 808.21/298.46 following rules strictly. 808.21/298.46 808.21/298.46 Trs: 808.21/298.46 { *(x, +(y, z)) -> +(*(x, y), *(x, z)) 808.21/298.46 , *(+(x, y), z) -> +(*(x, z), *(y, z)) } 808.21/298.46 808.21/298.46 The induced complexity on above rules (modulo remaining rules) is 808.21/298.46 YES(?,O(1)) . These rules are moved into the corresponding weak 808.21/298.46 component(s). 808.21/298.46 808.21/298.46 Sub-proof: 808.21/298.46 ---------- 808.21/298.46 We consider the following typing: 808.21/298.46 808.21/298.46 + :: (a,a) -> a 808.21/298.46 0 :: a 808.21/298.46 i :: a -> a 808.21/298.46 * :: (a,a) -> a 808.21/298.46 808.21/298.46 The following argument positions are considered usable: 808.21/298.46 808.21/298.46 Uargs(+) = {1, 2} 808.21/298.46 808.21/298.46 TcT has computed the following constructor-restricted 808.21/298.46 typedpolynomial interpretation. 808.21/298.46 808.21/298.46 [+](x1, x2) = 1 + x1 + x2 808.21/298.46 808.21/298.46 [0]() = 0 808.21/298.46 808.21/298.46 [i](x1) = 0 808.21/298.46 808.21/298.46 [*](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2 808.21/298.46 808.21/298.46 808.21/298.46 This order satisfies the following ordering constraints. 808.21/298.46 808.21/298.46 [+(x, 0())] = 1 + x 808.21/298.46 > x 808.21/298.46 = [x] 808.21/298.46 808.21/298.46 [+(x, i(x))] = 1 + x 808.21/298.46 > 808.21/298.46 = [0()] 808.21/298.46 808.21/298.46 [+(+(x, y), z)] = 2 + x + y + z 808.21/298.46 >= 2 + x + y + z 808.21/298.46 = [+(x, +(y, z))] 808.21/298.46 808.21/298.46 [*(x, +(y, z))] = 4*x + 2*x*y + 2*x*z + 2 + 2*y + 2*z 808.21/298.46 > 1 + 4*x + 2*x*y + 2*y + 2*x*z + 2*z 808.21/298.46 = [+(*(x, y), *(x, z))] 808.21/298.46 808.21/298.46 [*(+(x, y), z)] = 2 + 2*x + 2*y + 4*z + 2*x*z + 2*y*z 808.21/298.46 > 1 + 2*x + 2*x*z + 4*z + 2*y + 2*y*z 808.21/298.46 = [+(*(x, z), *(y, z))] 808.21/298.46 808.21/298.46 808.21/298.46 We return to the main proof. 808.21/298.46 808.21/298.46 We are left with following problem, upon which TcT provides the 808.21/298.46 certificate YES(O(1),O(1)). 808.21/298.46 808.21/298.46 Strict Trs: { +(+(x, y), z) -> +(x, +(y, z)) } 808.21/298.46 Weak Trs: 808.21/298.46 { +(x, 0()) -> x 808.21/298.46 , +(x, i(x)) -> 0() 808.21/298.46 , *(x, +(y, z)) -> +(*(x, y), *(x, z)) 808.21/298.46 , *(+(x, y), z) -> +(*(x, z), *(y, z)) } 808.21/298.46 Obligation: 808.21/298.46 runtime complexity 808.21/298.46 Answer: 808.21/298.46 YES(O(1),O(1)) 808.21/298.46 808.21/298.46 We use the processor 'polynomial interpretation' to orient 808.21/298.46 following rules strictly. 808.21/298.46 808.21/298.46 Trs: { +(+(x, y), z) -> +(x, +(y, z)) } 808.21/298.46 808.21/298.46 The induced complexity on above rules (modulo remaining rules) is 808.21/298.46 YES(?,O(1)) . These rules are moved into the corresponding weak 808.21/298.46 component(s). 808.21/298.46 808.21/298.46 Sub-proof: 808.21/298.46 ---------- 808.21/298.46 We consider the following typing: 808.21/298.46 808.21/298.46 + :: (a,a) -> a 808.21/298.46 0 :: a 808.21/298.46 i :: a -> a 808.21/298.46 * :: (a,a) -> a 808.21/298.46 808.21/298.46 The following argument positions are considered usable: 808.21/298.46 808.21/298.46 Uargs(+) = {1, 2} 808.21/298.46 808.21/298.46 TcT has computed the following constructor-restricted 808.21/298.46 typedpolynomial interpretation. 808.21/298.46 808.21/298.46 [+](x1, x2) = 1 + 2*x1 + x2 808.21/298.46 808.21/298.46 [0]() = 0 808.21/298.46 808.21/298.46 [i](x1) = 0 808.21/298.46 808.21/298.46 [*](x1, x2) = x1 + 2*x1*x2 + x2 808.21/298.46 808.21/298.46 808.21/298.46 This order satisfies the following ordering constraints. 808.21/298.46 808.21/298.46 [+(x, 0())] = 1 + 2*x 808.21/298.46 > x 808.21/298.46 = [x] 808.21/298.46 808.21/298.46 [+(x, i(x))] = 1 + 2*x 808.21/298.46 > 808.21/298.46 = [0()] 808.21/298.46 808.21/298.46 [+(+(x, y), z)] = 3 + 4*x + 2*y + z 808.21/298.46 > 2 + 2*x + 2*y + z 808.21/298.46 = [+(x, +(y, z))] 808.21/298.46 808.21/298.46 [*(x, +(y, z))] = 3*x + 4*x*y + 2*x*z + 1 + 2*y + z 808.21/298.46 >= 1 + 3*x + 4*x*y + 2*y + 2*x*z + z 808.21/298.46 = [+(*(x, y), *(x, z))] 808.21/298.46 808.21/298.46 [*(+(x, y), z)] = 1 + 2*x + y + 3*z + 4*x*z + 2*y*z 808.21/298.46 >= 1 + 2*x + 4*x*z + 3*z + y + 2*y*z 808.21/298.46 = [+(*(x, z), *(y, z))] 808.21/298.46 808.21/298.46 808.21/298.46 We return to the main proof. 808.21/298.46 808.21/298.46 We are left with following problem, upon which TcT provides the 808.21/298.46 certificate YES(O(1),O(1)). 808.21/298.46 808.21/298.46 Weak Trs: 808.21/298.46 { +(x, 0()) -> x 808.21/298.46 , +(x, i(x)) -> 0() 808.21/298.46 , +(+(x, y), z) -> +(x, +(y, z)) 808.21/298.46 , *(x, +(y, z)) -> +(*(x, y), *(x, z)) 808.21/298.46 , *(+(x, y), z) -> +(*(x, z), *(y, z)) } 808.21/298.46 Obligation: 808.21/298.46 runtime complexity 808.21/298.46 Answer: 808.21/298.46 YES(O(1),O(1)) 808.21/298.46 808.21/298.46 Empty rules are trivially bounded 808.21/298.46 808.21/298.46 Hurray, we answered YES(O(1),O(n^1)) 808.57/298.69 EOF