YES(O(1),O(n^2)) 12.31/4.99 YES(O(1),O(n^2)) 12.31/4.99 12.31/4.99 We are left with following problem, upon which TcT provides the 12.31/4.99 certificate YES(O(1),O(n^2)). 12.31/4.99 12.31/4.99 Strict Trs: 12.31/4.99 { *(x, +(y, z)) -> +(*(x, y), *(x, z)) 12.31/4.99 , *(x, 1()) -> x 12.31/4.99 , *(+(x, y), z) -> +(*(x, z), *(y, z)) 12.31/4.99 , *(1(), y) -> y } 12.31/4.99 Obligation: 12.31/4.99 runtime complexity 12.31/4.99 Answer: 12.31/4.99 YES(O(1),O(n^2)) 12.31/4.99 12.31/4.99 We add the following weak dependency pairs: 12.31/4.99 12.31/4.99 Strict DPs: 12.31/4.99 { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) 12.31/4.99 , *^#(x, 1()) -> c_2(x) 12.31/4.99 , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) 12.31/4.99 , *^#(1(), y) -> c_4(y) } 12.31/4.99 12.31/4.99 and mark the set of starting terms. 12.31/4.99 12.31/4.99 We are left with following problem, upon which TcT provides the 12.31/4.99 certificate YES(O(1),O(n^2)). 12.31/4.99 12.31/4.99 Strict DPs: 12.31/4.99 { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) 12.31/4.99 , *^#(x, 1()) -> c_2(x) 12.31/4.99 , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) 12.31/4.99 , *^#(1(), y) -> c_4(y) } 12.31/4.99 Strict Trs: 12.31/4.99 { *(x, +(y, z)) -> +(*(x, y), *(x, z)) 12.31/4.99 , *(x, 1()) -> x 12.31/4.99 , *(+(x, y), z) -> +(*(x, z), *(y, z)) 12.31/4.99 , *(1(), y) -> y } 12.31/4.99 Obligation: 12.31/4.99 runtime complexity 12.31/4.99 Answer: 12.31/4.99 YES(O(1),O(n^2)) 12.31/4.99 12.31/4.99 No rule is usable, rules are removed from the input problem. 12.31/4.99 12.31/4.99 We are left with following problem, upon which TcT provides the 12.31/4.99 certificate YES(O(1),O(n^2)). 12.31/4.99 12.31/4.99 Strict DPs: 12.31/4.99 { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) 12.31/4.99 , *^#(x, 1()) -> c_2(x) 12.31/4.99 , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) 12.31/4.99 , *^#(1(), y) -> c_4(y) } 12.31/4.99 Obligation: 12.31/4.99 runtime complexity 12.31/4.99 Answer: 12.31/4.99 YES(O(1),O(n^2)) 12.31/4.99 12.31/4.99 The weightgap principle applies (using the following constant 12.31/4.99 growth matrix-interpretation) 12.31/4.99 12.31/4.99 The following argument positions are usable: 12.31/4.99 Uargs(c_1) = {1, 2}, Uargs(c_3) = {1, 2} 12.31/4.99 12.31/4.99 TcT has computed the following constructor-restricted matrix 12.31/4.99 interpretation. 12.31/4.99 12.31/4.99 [+](x1, x2) = [1 2] x1 + [1 2] x2 + [0] 12.31/4.99 [0 1] [0 1] [0] 12.31/4.99 12.31/4.99 [1] = [0] 12.31/4.99 [0] 12.31/4.99 12.31/4.99 [*^#](x1, x2) = [1] 12.31/4.99 [0] 12.31/4.99 12.31/4.99 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 12.31/4.99 [0 1] [0 1] [2] 12.31/4.99 12.31/4.99 [c_2](x1) = [0] 12.31/4.99 [0] 12.31/4.99 12.31/4.99 [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 12.31/4.99 [0 1] [0 1] [2] 12.31/4.99 12.31/4.99 [c_4](x1) = [0] 12.31/4.99 [0] 12.31/4.99 12.31/4.99 The order satisfies the following ordering constraints: 12.31/4.99 12.31/4.99 [*^#(x, +(y, z))] = [1] 12.31/4.99 [0] 12.31/4.99 ? [3] 12.31/4.99 [2] 12.31/4.99 = [c_1(*^#(x, y), *^#(x, z))] 12.31/4.99 12.31/4.99 [*^#(x, 1())] = [1] 12.31/4.99 [0] 12.31/4.99 > [0] 12.31/4.99 [0] 12.31/4.99 = [c_2(x)] 12.31/4.99 12.31/4.99 [*^#(+(x, y), z)] = [1] 12.31/4.99 [0] 12.31/4.99 ? [3] 12.31/4.99 [2] 12.31/4.99 = [c_3(*^#(x, z), *^#(y, z))] 12.31/4.99 12.31/4.99 [*^#(1(), y)] = [1] 12.31/4.99 [0] 12.31/4.99 > [0] 12.31/4.99 [0] 12.31/4.99 = [c_4(y)] 12.31/4.99 12.31/4.99 12.31/4.99 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 12.31/4.99 12.31/4.99 We are left with following problem, upon which TcT provides the 12.31/4.99 certificate YES(O(1),O(n^2)). 12.31/4.99 12.31/4.99 Strict DPs: 12.31/4.99 { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) 12.31/4.99 , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) } 12.31/4.99 Weak DPs: 12.31/4.99 { *^#(x, 1()) -> c_2(x) 12.31/4.99 , *^#(1(), y) -> c_4(y) } 12.31/4.99 Obligation: 12.31/4.99 runtime complexity 12.31/4.99 Answer: 12.31/4.99 YES(O(1),O(n^2)) 12.31/4.99 12.31/4.99 We use the processor 'polynomial interpretation' to orient 12.31/4.99 following rules strictly. 12.31/4.99 12.31/4.99 DPs: 12.31/4.99 { 1: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) } 12.31/4.99 12.31/4.99 Sub-proof: 12.31/4.99 ---------- 12.31/4.99 We consider the following typing: 12.31/4.99 12.31/4.99 + :: (a,a) -> a 12.31/4.99 1 :: a 12.31/4.99 *^# :: (a,a) -> b 12.31/4.99 c_1 :: (b,b) -> b 12.31/4.99 c_2 :: a -> b 12.31/4.99 c_3 :: (b,b) -> b 12.31/4.99 c_4 :: a -> b 12.31/4.99 12.31/4.99 The following argument positions are considered usable: 12.31/4.99 12.31/4.99 Uargs(c_1) = {1, 2}, Uargs(c_3) = {1, 2} 12.31/4.99 12.31/4.99 TcT has computed the following constructor-restricted 12.31/4.99 typedpolynomial interpretation. 12.31/4.99 12.31/4.99 [+](x1, x2) = 1 + x1 + x2 12.31/4.99 12.31/4.99 [1]() = 0 12.31/4.99 12.31/4.99 [*^#](x1, x2) = x1*x2 + x2 12.31/4.99 12.31/4.99 [c_1](x1, x2) = x1 + x2 12.31/4.99 12.31/4.99 [c_2](x1) = 0 12.31/4.99 12.31/4.99 [c_3](x1, x2) = x1 + x2 12.31/4.99 12.31/4.99 [c_4](x1) = x1 12.31/4.99 12.31/4.99 12.31/4.99 This order satisfies the following ordering constraints. 12.31/4.99 12.31/4.99 [*^#(x, +(y, z))] = x + x*y + x*z + 1 + y + z 12.31/4.99 > x*y + y + x*z + z 12.31/4.99 = [c_1(*^#(x, y), *^#(x, z))] 12.31/4.99 12.31/4.99 [*^#(x, 1())] = 12.31/4.99 >= 12.31/4.99 = [c_2(x)] 12.31/4.99 12.31/4.99 [*^#(+(x, y), z)] = 2*z + x*z + y*z 12.31/4.99 >= x*z + 2*z + y*z 12.31/4.99 = [c_3(*^#(x, z), *^#(y, z))] 12.31/4.99 12.31/4.99 [*^#(1(), y)] = y 12.31/4.99 >= y 12.31/4.99 = [c_4(y)] 12.31/4.99 12.31/4.99 12.31/4.99 The strictly oriented rules are moved into the weak component. 12.31/4.99 12.31/4.99 We are left with following problem, upon which TcT provides the 12.31/4.99 certificate YES(O(1),O(n^2)). 12.31/4.99 12.31/4.99 Strict DPs: { *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) } 12.31/4.99 Weak DPs: 12.31/4.99 { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) 12.31/4.99 , *^#(x, 1()) -> c_2(x) 12.31/4.99 , *^#(1(), y) -> c_4(y) } 12.31/4.99 Obligation: 12.31/4.99 runtime complexity 12.31/4.99 Answer: 12.31/4.99 YES(O(1),O(n^2)) 12.31/4.99 12.31/4.99 We use the processor 'polynomial interpretation' to orient 12.31/4.99 following rules strictly. 12.31/4.99 12.31/4.99 DPs: 12.31/4.99 { 1: *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) } 12.31/4.99 12.31/4.99 Sub-proof: 12.31/4.99 ---------- 12.31/4.99 We consider the following typing: 12.31/4.99 12.31/4.99 + :: (a,a) -> a 12.31/4.99 1 :: a 12.31/4.99 *^# :: (a,a) -> b 12.31/4.99 c_1 :: (b,b) -> b 12.31/4.99 c_2 :: a -> b 12.31/4.99 c_3 :: (b,b) -> b 12.31/4.99 c_4 :: a -> b 12.31/4.99 12.31/4.99 The following argument positions are considered usable: 12.31/4.99 12.31/4.99 Uargs(c_1) = {1, 2}, Uargs(c_3) = {1, 2} 12.31/4.99 12.31/4.99 TcT has computed the following constructor-restricted 12.31/4.99 typedpolynomial interpretation. 12.31/4.99 12.31/4.99 [+](x1, x2) = 2 + x1 + x2 12.31/4.99 12.31/4.99 [1]() = 0 12.31/4.99 12.31/4.99 [*^#](x1, x2) = 2*x1 + x1*x2 12.31/4.99 12.31/4.99 [c_1](x1, x2) = x1 + x2 12.31/4.99 12.31/4.99 [c_2](x1) = x1 12.31/4.99 12.31/4.99 [c_3](x1, x2) = x1 + x2 12.31/4.99 12.31/4.99 [c_4](x1) = 0 12.31/4.99 12.31/4.99 12.31/4.99 This order satisfies the following ordering constraints. 12.31/4.99 12.31/4.99 [*^#(x, +(y, z))] = 4*x + x*y + x*z 12.31/4.99 >= 4*x + x*y + x*z 12.31/4.99 = [c_1(*^#(x, y), *^#(x, z))] 12.31/4.99 12.31/4.99 [*^#(x, 1())] = 2*x 12.31/4.99 >= x 12.31/4.99 = [c_2(x)] 12.31/4.99 12.31/4.99 [*^#(+(x, y), z)] = 4 + 2*x + 2*y + 2*z + x*z + y*z 12.31/4.99 > 2*x + x*z + 2*y + y*z 12.31/4.99 = [c_3(*^#(x, z), *^#(y, z))] 12.31/4.99 12.31/4.99 [*^#(1(), y)] = 12.31/4.99 >= 12.31/4.99 = [c_4(y)] 12.31/4.99 12.31/4.99 12.31/4.99 The strictly oriented rules are moved into the weak component. 12.31/4.99 12.31/4.99 We are left with following problem, upon which TcT provides the 12.31/4.99 certificate YES(O(1),O(1)). 12.31/4.99 12.31/4.99 Weak DPs: 12.31/4.99 { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) 12.31/4.99 , *^#(x, 1()) -> c_2(x) 12.31/4.99 , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) 12.31/4.99 , *^#(1(), y) -> c_4(y) } 12.31/4.99 Obligation: 12.31/4.99 runtime complexity 12.31/4.99 Answer: 12.31/4.99 YES(O(1),O(1)) 12.31/4.99 12.31/4.99 The following weak DPs constitute a sub-graph of the DG that is 12.31/4.99 closed under successors. The DPs are removed. 12.31/4.99 12.31/4.99 { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) 12.31/4.99 , *^#(x, 1()) -> c_2(x) 12.31/4.99 , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) 12.31/4.99 , *^#(1(), y) -> c_4(y) } 12.31/4.99 12.31/4.99 We are left with following problem, upon which TcT provides the 12.31/4.99 certificate YES(O(1),O(1)). 12.31/4.99 12.31/4.99 Rules: Empty 12.31/4.99 Obligation: 12.31/4.99 runtime complexity 12.31/4.99 Answer: 12.31/4.99 YES(O(1),O(1)) 12.31/4.99 12.31/4.99 Empty rules are trivially bounded 12.31/4.99 12.31/4.99 Hurray, we answered YES(O(1),O(n^2)) 12.55/5.00 EOF