MAYBE 368.30/210.19 MAYBE 368.30/210.19 368.30/210.19 We are left with following problem, upon which TcT provides the 368.30/210.19 certificate MAYBE. 368.30/210.19 368.30/210.19 Strict Trs: 368.30/210.19 { +(0(), y) -> y 368.30/210.19 , +(s(x), y) -> s(+(x, y)) 368.30/210.19 , +(p(x), y) -> p(+(x, y)) 368.30/210.19 , minus(0()) -> 0() 368.30/210.19 , minus(s(x)) -> p(minus(x)) 368.30/210.19 , minus(p(x)) -> s(minus(x)) 368.30/210.19 , *(0(), y) -> 0() 368.30/210.19 , *(s(x), y) -> +(*(x, y), y) 368.30/210.19 , *(p(x), y) -> +(*(x, y), minus(y)) } 368.30/210.19 Obligation: 368.30/210.19 runtime complexity 368.30/210.19 Answer: 368.30/210.19 MAYBE 368.30/210.19 368.30/210.19 None of the processors succeeded. 368.30/210.19 368.30/210.19 Details of failed attempt(s): 368.30/210.19 ----------------------------- 368.30/210.19 1) 'Best' failed due to the following reason: 368.30/210.19 368.30/210.19 None of the processors succeeded. 368.30/210.19 368.30/210.19 Details of failed attempt(s): 368.30/210.19 ----------------------------- 368.30/210.19 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 368.30/210.19 seconds)' failed due to the following reason: 368.30/210.19 368.30/210.19 None of the processors succeeded. 368.30/210.19 368.30/210.19 Details of failed attempt(s): 368.30/210.19 ----------------------------- 368.30/210.19 1) 'empty' failed due to the following reason: 368.30/210.19 368.30/210.19 Empty strict component of the problem is NOT empty. 368.30/210.19 368.30/210.19 2) 'With Problem ...' failed due to the following reason: 368.30/210.19 368.30/210.19 None of the processors succeeded. 368.30/210.19 368.30/210.19 Details of failed attempt(s): 368.30/210.19 ----------------------------- 368.30/210.19 1) 'empty' failed due to the following reason: 368.30/210.19 368.30/210.19 Empty strict component of the problem is NOT empty. 368.30/210.19 368.30/210.19 2) 'Fastest' failed due to the following reason: 368.30/210.19 368.30/210.19 None of the processors succeeded. 368.30/210.19 368.30/210.19 Details of failed attempt(s): 368.30/210.19 ----------------------------- 368.30/210.19 1) 'With Problem ...' failed due to the following reason: 368.30/210.19 368.30/210.19 We use the processor 'polynomial interpretation' to orient 368.30/210.19 following rules strictly. 368.30/210.19 368.30/210.19 Trs: 368.30/210.19 { *(s(x), y) -> +(*(x, y), y) 368.30/210.19 , *(p(x), y) -> +(*(x, y), minus(y)) } 368.30/210.19 368.30/210.19 The induced complexity on above rules (modulo remaining rules) is 368.30/210.19 YES(?,O(n^2)) . These rules are moved into the corresponding weak 368.30/210.19 component(s). 368.30/210.19 368.30/210.19 Sub-proof: 368.30/210.19 ---------- 368.30/210.19 We consider the following typing: 368.30/210.19 368.30/210.19 + :: (a,a) -> a 368.30/210.19 0 :: a 368.30/210.19 s :: a -> a 368.30/210.19 p :: a -> a 368.30/210.19 minus :: a -> a 368.30/210.19 * :: (a,a) -> a 368.30/210.19 368.30/210.19 The following argument positions are considered usable: 368.30/210.19 368.30/210.19 Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} 368.30/210.19 368.30/210.19 TcT has computed the following constructor-restricted 368.30/210.19 typedpolynomial interpretation. 368.30/210.19 368.30/210.19 [+](x1, x2) = x1 + x2 368.30/210.19 368.30/210.19 [0]() = 0 368.30/210.19 368.30/210.19 [s](x1) = 1 + x1 368.30/210.19 368.30/210.19 [p](x1) = 1 + x1 368.30/210.19 368.30/210.19 [minus](x1) = x1 368.30/210.19 368.30/210.19 [*](x1, x2) = x1*x2 + x1^2 368.30/210.19 368.30/210.19 368.30/210.19 This order satisfies the following ordering constraints. 368.30/210.19 368.30/210.19 [+(0(), y)] = y 368.30/210.19 >= y 368.30/210.19 = [y] 368.30/210.19 368.30/210.19 [+(s(x), y)] = 1 + x + y 368.30/210.19 >= 1 + x + y 368.30/210.19 = [s(+(x, y))] 368.30/210.19 368.30/210.19 [+(p(x), y)] = 1 + x + y 368.30/210.19 >= 1 + x + y 368.30/210.19 = [p(+(x, y))] 368.30/210.19 368.30/210.19 [minus(0())] = 368.30/210.19 >= 368.30/210.19 = [0()] 368.30/210.19 368.30/210.19 [minus(s(x))] = 1 + x 368.30/210.19 >= 1 + x 368.30/210.19 = [p(minus(x))] 368.30/210.19 368.30/210.19 [minus(p(x))] = 1 + x 368.30/210.19 >= 1 + x 368.30/210.19 = [s(minus(x))] 368.30/210.19 368.30/210.19 [*(0(), y)] = 368.30/210.19 >= 368.30/210.19 = [0()] 368.30/210.19 368.30/210.19 [*(s(x), y)] = y + x*y + 1 + 2*x + x^2 368.30/210.19 > x*y + x^2 + y 368.30/210.19 = [+(*(x, y), y)] 368.30/210.19 368.30/210.19 [*(p(x), y)] = y + x*y + 1 + 2*x + x^2 368.30/210.19 > x*y + x^2 + y 368.30/210.19 = [+(*(x, y), minus(y))] 368.30/210.19 368.30/210.19 368.30/210.19 We return to the main proof. 368.30/210.19 368.30/210.19 We are left with following problem, upon which TcT provides the 368.30/210.19 certificate MAYBE. 368.30/210.19 368.30/210.19 Strict Trs: 368.30/210.19 { +(0(), y) -> y 368.30/210.19 , +(s(x), y) -> s(+(x, y)) 368.30/210.19 , +(p(x), y) -> p(+(x, y)) 368.30/210.19 , minus(0()) -> 0() 368.30/210.19 , minus(s(x)) -> p(minus(x)) 368.30/210.19 , minus(p(x)) -> s(minus(x)) 368.30/210.19 , *(0(), y) -> 0() } 368.30/210.19 Weak Trs: 368.30/210.19 { *(s(x), y) -> +(*(x, y), y) 368.30/210.19 , *(p(x), y) -> +(*(x, y), minus(y)) } 368.30/210.19 Obligation: 368.30/210.19 runtime complexity 368.30/210.19 Answer: 368.30/210.19 MAYBE 368.30/210.19 368.30/210.19 We use the processor 'polynomial interpretation' to orient 368.30/210.19 following rules strictly. 368.30/210.19 368.30/210.19 Trs: { *(0(), y) -> 0() } 368.30/210.19 368.30/210.19 The induced complexity on above rules (modulo remaining rules) is 368.30/210.19 YES(?,O(n^2)) . These rules are moved into the corresponding weak 368.30/210.19 component(s). 368.30/210.19 368.30/210.19 Sub-proof: 368.30/210.19 ---------- 368.30/210.19 We consider the following typing: 368.30/210.19 368.30/210.19 + :: (a,a) -> a 368.30/210.19 0 :: a 368.30/210.19 s :: a -> a 368.30/210.19 p :: a -> a 368.30/210.19 minus :: a -> a 368.30/210.19 * :: (a,a) -> a 368.30/210.19 368.30/210.19 The following argument positions are considered usable: 368.30/210.19 368.30/210.19 Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} 368.30/210.19 368.30/210.19 TcT has computed the following constructor-restricted 368.30/210.19 typedpolynomial interpretation. 368.30/210.19 368.30/210.19 [+](x1, x2) = x1 + x2 368.30/210.19 368.30/210.19 [0]() = 0 368.30/210.19 368.30/210.19 [s](x1) = 1 + x1 368.30/210.19 368.30/210.19 [p](x1) = 1 + x1 368.30/210.19 368.30/210.19 [minus](x1) = x1 368.30/210.19 368.30/210.19 [*](x1, x2) = 1 + x1*x2 368.30/210.19 368.30/210.19 368.30/210.19 This order satisfies the following ordering constraints. 368.30/210.19 368.30/210.19 [+(0(), y)] = y 368.30/210.19 >= y 368.30/210.19 = [y] 368.30/210.19 368.30/210.19 [+(s(x), y)] = 1 + x + y 368.30/210.19 >= 1 + x + y 368.30/210.19 = [s(+(x, y))] 368.30/210.19 368.30/210.19 [+(p(x), y)] = 1 + x + y 368.30/210.19 >= 1 + x + y 368.30/210.19 = [p(+(x, y))] 368.30/210.19 368.30/210.19 [minus(0())] = 368.30/210.19 >= 368.30/210.19 = [0()] 368.30/210.19 368.30/210.19 [minus(s(x))] = 1 + x 368.30/210.19 >= 1 + x 368.30/210.19 = [p(minus(x))] 368.30/210.19 368.30/210.19 [minus(p(x))] = 1 + x 368.30/210.19 >= 1 + x 368.30/210.19 = [s(minus(x))] 368.30/210.19 368.30/210.19 [*(0(), y)] = 1 368.30/210.19 > 368.30/210.19 = [0()] 368.30/210.19 368.30/210.19 [*(s(x), y)] = 1 + y + x*y 368.30/210.19 >= 1 + x*y + y 368.30/210.19 = [+(*(x, y), y)] 368.30/210.19 368.30/210.19 [*(p(x), y)] = 1 + y + x*y 368.30/210.19 >= 1 + x*y + y 368.30/210.19 = [+(*(x, y), minus(y))] 368.30/210.19 368.30/210.19 368.30/210.19 We return to the main proof. 368.30/210.19 368.30/210.19 We are left with following problem, upon which TcT provides the 368.30/210.19 certificate MAYBE. 368.30/210.19 368.30/210.19 Strict Trs: 368.30/210.19 { +(0(), y) -> y 368.30/210.19 , +(s(x), y) -> s(+(x, y)) 368.30/210.19 , +(p(x), y) -> p(+(x, y)) 368.30/210.19 , minus(0()) -> 0() 368.30/210.19 , minus(s(x)) -> p(minus(x)) 368.30/210.19 , minus(p(x)) -> s(minus(x)) } 368.30/210.19 Weak Trs: 368.30/210.19 { *(0(), y) -> 0() 368.30/210.19 , *(s(x), y) -> +(*(x, y), y) 368.30/210.19 , *(p(x), y) -> +(*(x, y), minus(y)) } 368.30/210.19 Obligation: 368.30/210.19 runtime complexity 368.30/210.19 Answer: 368.30/210.19 MAYBE 368.30/210.19 368.30/210.19 We use the processor 'polynomial interpretation' to orient 368.30/210.19 following rules strictly. 368.30/210.19 368.30/210.19 Trs: { +(0(), y) -> y } 368.30/210.19 368.30/210.19 The induced complexity on above rules (modulo remaining rules) is 368.30/210.19 YES(?,O(n^2)) . These rules are moved into the corresponding weak 368.30/210.19 component(s). 368.30/210.19 368.30/210.19 Sub-proof: 368.30/210.19 ---------- 368.30/210.19 We consider the following typing: 368.30/210.19 368.30/210.19 + :: (a,a) -> a 368.30/210.19 0 :: a 368.30/210.19 s :: a -> a 368.30/210.19 p :: a -> a 368.30/210.19 minus :: a -> a 368.30/210.19 * :: (a,a) -> a 368.30/210.19 368.30/210.19 The following argument positions are considered usable: 368.30/210.19 368.30/210.19 Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} 368.30/210.19 368.30/210.19 TcT has computed the following constructor-restricted 368.30/210.19 typedpolynomial interpretation. 368.30/210.19 368.30/210.19 [+](x1, x2) = 3 + x1 + x2 368.30/210.19 368.30/210.19 [0]() = 0 368.30/210.19 368.30/210.19 [s](x1) = 1 + x1 368.30/210.19 368.30/210.19 [p](x1) = 1 + x1 368.30/210.19 368.30/210.19 [minus](x1) = x1 368.30/210.19 368.30/210.19 [*](x1, x2) = 2*x1 + x1*x2 + 2*x1^2 368.30/210.19 368.30/210.19 368.30/210.19 This order satisfies the following ordering constraints. 368.30/210.19 368.30/210.19 [+(0(), y)] = 3 + y 368.30/210.19 > y 368.30/210.19 = [y] 368.30/210.19 368.30/210.19 [+(s(x), y)] = 4 + x + y 368.30/210.19 >= 4 + x + y 368.30/210.19 = [s(+(x, y))] 368.30/210.19 368.30/210.19 [+(p(x), y)] = 4 + x + y 368.30/210.19 >= 4 + x + y 368.30/210.19 = [p(+(x, y))] 368.30/210.19 368.30/210.19 [minus(0())] = 368.30/210.19 >= 368.30/210.19 = [0()] 368.30/210.19 368.30/210.19 [minus(s(x))] = 1 + x 368.30/210.19 >= 1 + x 368.30/210.19 = [p(minus(x))] 368.30/210.19 368.30/210.19 [minus(p(x))] = 1 + x 368.30/210.19 >= 1 + x 368.30/210.19 = [s(minus(x))] 368.30/210.19 368.30/210.19 [*(0(), y)] = 368.30/210.19 >= 368.30/210.19 = [0()] 368.30/210.19 368.30/210.19 [*(s(x), y)] = 4 + 6*x + y + x*y + 2*x^2 368.30/210.19 > 3 + 2*x + x*y + 2*x^2 + y 368.30/210.19 = [+(*(x, y), y)] 368.30/210.19 368.30/210.19 [*(p(x), y)] = 4 + 6*x + y + x*y + 2*x^2 368.30/210.19 > 3 + 2*x + x*y + 2*x^2 + y 368.30/210.19 = [+(*(x, y), minus(y))] 368.30/210.19 368.30/210.19 368.30/210.19 We return to the main proof. 368.30/210.19 368.30/210.19 We are left with following problem, upon which TcT provides the 368.30/210.19 certificate MAYBE. 368.30/210.19 368.30/210.19 Strict Trs: 368.30/210.19 { +(s(x), y) -> s(+(x, y)) 368.30/210.19 , +(p(x), y) -> p(+(x, y)) 368.30/210.19 , minus(0()) -> 0() 368.30/210.19 , minus(s(x)) -> p(minus(x)) 368.30/210.19 , minus(p(x)) -> s(minus(x)) } 368.30/210.19 Weak Trs: 368.30/210.19 { +(0(), y) -> y 368.30/210.19 , *(0(), y) -> 0() 368.30/210.19 , *(s(x), y) -> +(*(x, y), y) 368.30/210.19 , *(p(x), y) -> +(*(x, y), minus(y)) } 368.30/210.19 Obligation: 368.30/210.19 runtime complexity 368.30/210.19 Answer: 368.30/210.19 MAYBE 368.30/210.19 368.30/210.19 We use the processor 'polynomial interpretation' to orient 368.30/210.19 following rules strictly. 368.30/210.19 368.30/210.19 Trs: 368.30/210.19 { minus(0()) -> 0() 368.30/210.19 , minus(s(x)) -> p(minus(x)) 368.30/210.19 , minus(p(x)) -> s(minus(x)) } 368.30/210.19 368.30/210.19 The induced complexity on above rules (modulo remaining rules) is 368.30/210.19 YES(?,O(n^2)) . These rules are moved into the corresponding weak 368.30/210.19 component(s). 368.47/210.20 368.47/210.20 Sub-proof: 368.47/210.20 ---------- 368.47/210.20 We consider the following typing: 368.47/210.20 368.47/210.20 + :: (a,a) -> a 368.47/210.20 0 :: a 368.47/210.20 s :: a -> a 368.47/210.20 p :: a -> a 368.47/210.20 minus :: a -> a 368.47/210.20 * :: (a,a) -> a 368.47/210.20 368.47/210.20 The following argument positions are considered usable: 368.47/210.20 368.47/210.20 Uargs(+) = {1, 2}, Uargs(s) = {1}, Uargs(p) = {1} 368.47/210.20 368.47/210.20 TcT has computed the following constructor-restricted 368.47/210.20 typedpolynomial interpretation. 368.47/210.20 368.47/210.20 [+](x1, x2) = x1 + x2 368.47/210.20 368.47/210.20 [0]() = 1 368.47/210.20 368.47/210.20 [s](x1) = 1 + x1 368.47/210.20 368.47/210.20 [p](x1) = 1 + x1 368.47/210.20 368.47/210.20 [minus](x1) = 2 + 2*x1 368.47/210.20 368.47/210.20 [*](x1, x2) = 1 + 2*x1 + 2*x1*x2 + x1^2 + 2*x2 368.47/210.20 368.47/210.20 368.47/210.20 This order satisfies the following ordering constraints. 368.47/210.20 368.47/210.20 [+(0(), y)] = 1 + y 368.47/210.20 > y 368.47/210.20 = [y] 368.47/210.20 368.47/210.20 [+(s(x), y)] = 1 + x + y 368.47/210.20 >= 1 + x + y 368.47/210.20 = [s(+(x, y))] 368.47/210.20 368.47/210.20 [+(p(x), y)] = 1 + x + y 368.47/210.20 >= 1 + x + y 368.47/210.20 = [p(+(x, y))] 368.47/210.20 368.47/210.20 [minus(0())] = 4 368.47/210.20 > 1 368.47/210.20 = [0()] 368.47/210.20 368.47/210.20 [minus(s(x))] = 4 + 2*x 368.47/210.20 > 3 + 2*x 368.47/210.20 = [p(minus(x))] 368.47/210.20 368.47/210.20 [minus(p(x))] = 4 + 2*x 368.47/210.20 > 3 + 2*x 368.47/210.20 = [s(minus(x))] 368.47/210.20 368.47/210.20 [*(0(), y)] = 4 + 4*y 368.47/210.20 > 1 368.47/210.20 = [0()] 368.47/210.20 368.47/210.20 [*(s(x), y)] = 4 + 4*x + 4*y + 2*x*y + x^2 368.47/210.20 > 1 + 2*x + 2*x*y + x^2 + 3*y 368.47/210.20 = [+(*(x, y), y)] 368.47/210.20 368.47/210.20 [*(p(x), y)] = 4 + 4*x + 4*y + 2*x*y + x^2 368.47/210.20 > 3 + 2*x + 2*x*y + x^2 + 4*y 368.47/210.20 = [+(*(x, y), minus(y))] 368.47/210.20 368.47/210.20 368.47/210.20 We return to the main proof. 368.47/210.20 368.47/210.20 We are left with following problem, upon which TcT provides the 368.47/210.20 certificate MAYBE. 368.47/210.20 368.47/210.20 Strict Trs: 368.47/210.20 { +(s(x), y) -> s(+(x, y)) 368.47/210.20 , +(p(x), y) -> p(+(x, y)) } 368.47/210.20 Weak Trs: 368.47/210.20 { +(0(), y) -> y 368.47/210.20 , minus(0()) -> 0() 368.47/210.20 , minus(s(x)) -> p(minus(x)) 368.47/210.20 , minus(p(x)) -> s(minus(x)) 368.47/210.20 , *(0(), y) -> 0() 368.47/210.20 , *(s(x), y) -> +(*(x, y), y) 368.47/210.20 , *(p(x), y) -> +(*(x, y), minus(y)) } 368.47/210.20 Obligation: 368.47/210.20 runtime complexity 368.47/210.20 Answer: 368.47/210.20 MAYBE 368.47/210.20 368.47/210.20 None of the processors succeeded. 368.47/210.20 368.47/210.20 Details of failed attempt(s): 368.47/210.20 ----------------------------- 368.47/210.20 1) 'empty' failed due to the following reason: 368.47/210.20 368.47/210.20 Empty strict component of the problem is NOT empty. 368.47/210.20 368.47/210.20 2) 'With Problem ...' failed due to the following reason: 368.47/210.20 368.47/210.20 Empty strict component of the problem is NOT empty. 368.47/210.20 368.47/210.20 368.47/210.20 2) 'With Problem ...' failed due to the following reason: 368.47/210.20 368.47/210.20 None of the processors succeeded. 368.47/210.20 368.47/210.20 Details of failed attempt(s): 368.47/210.20 ----------------------------- 368.47/210.20 1) 'empty' failed due to the following reason: 368.47/210.20 368.47/210.20 Empty strict component of the problem is NOT empty. 368.47/210.20 368.47/210.20 2) 'With Problem ...' failed due to the following reason: 368.47/210.20 368.47/210.20 None of the processors succeeded. 368.47/210.20 368.47/210.20 Details of failed attempt(s): 368.47/210.20 ----------------------------- 368.47/210.20 1) 'empty' failed due to the following reason: 368.47/210.20 368.47/210.20 Empty strict component of the problem is NOT empty. 368.47/210.20 368.47/210.20 2) 'With Problem ...' failed due to the following reason: 368.47/210.20 368.47/210.20 None of the processors succeeded. 368.47/210.20 368.47/210.20 Details of failed attempt(s): 368.47/210.20 ----------------------------- 368.47/210.20 1) 'empty' failed due to the following reason: 368.47/210.20 368.47/210.20 Empty strict component of the problem is NOT empty. 368.47/210.20 368.47/210.20 2) 'With Problem ...' failed due to the following reason: 368.47/210.20 368.47/210.20 Empty strict component of the problem is NOT empty. 368.47/210.20 368.47/210.20 368.47/210.20 368.47/210.20 368.47/210.20 368.47/210.20 368.47/210.20 368.47/210.20 2) 'Best' failed due to the following reason: 368.47/210.20 368.47/210.20 None of the processors succeeded. 368.47/210.20 368.47/210.20 Details of failed attempt(s): 368.47/210.20 ----------------------------- 368.47/210.20 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 368.47/210.20 following reason: 368.47/210.20 368.47/210.20 The processor is inapplicable, reason: 368.47/210.20 Processor only applicable for innermost runtime complexity analysis 368.47/210.20 368.47/210.20 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 368.47/210.20 to the following reason: 368.47/210.20 368.47/210.20 The processor is inapplicable, reason: 368.47/210.20 Processor only applicable for innermost runtime complexity analysis 368.47/210.20 368.47/210.20 368.47/210.20 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 368.47/210.20 failed due to the following reason: 368.47/210.20 368.47/210.20 None of the processors succeeded. 368.47/210.20 368.47/210.20 Details of failed attempt(s): 368.47/210.20 ----------------------------- 368.47/210.20 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 368.47/210.20 failed due to the following reason: 368.47/210.20 368.47/210.20 match-boundness of the problem could not be verified. 368.47/210.20 368.47/210.20 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 368.47/210.20 failed due to the following reason: 368.47/210.20 368.47/210.20 match-boundness of the problem could not be verified. 368.47/210.20 368.47/210.20 368.47/210.20 368.47/210.20 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 368.47/210.20 the following reason: 368.47/210.20 368.47/210.20 We add the following weak dependency pairs: 368.47/210.20 368.47/210.20 Strict DPs: 368.47/210.20 { +^#(0(), y) -> c_1(y) 368.47/210.20 , +^#(s(x), y) -> c_2(+^#(x, y)) 368.47/210.20 , +^#(p(x), y) -> c_3(+^#(x, y)) 368.47/210.20 , minus^#(0()) -> c_4() 368.47/210.20 , minus^#(s(x)) -> c_5(minus^#(x)) 368.47/210.20 , minus^#(p(x)) -> c_6(minus^#(x)) 368.47/210.20 , *^#(0(), y) -> c_7() 368.47/210.20 , *^#(s(x), y) -> c_8(+^#(*(x, y), y)) 368.47/210.20 , *^#(p(x), y) -> c_9(+^#(*(x, y), minus(y))) } 368.47/210.20 368.47/210.20 and mark the set of starting terms. 368.47/210.20 368.47/210.20 We are left with following problem, upon which TcT provides the 368.47/210.20 certificate MAYBE. 368.47/210.20 368.47/210.20 Strict DPs: 368.47/210.20 { +^#(0(), y) -> c_1(y) 368.47/210.20 , +^#(s(x), y) -> c_2(+^#(x, y)) 368.47/210.20 , +^#(p(x), y) -> c_3(+^#(x, y)) 368.47/210.20 , minus^#(0()) -> c_4() 368.47/210.20 , minus^#(s(x)) -> c_5(minus^#(x)) 368.47/210.20 , minus^#(p(x)) -> c_6(minus^#(x)) 368.47/210.20 , *^#(0(), y) -> c_7() 368.47/210.20 , *^#(s(x), y) -> c_8(+^#(*(x, y), y)) 368.47/210.20 , *^#(p(x), y) -> c_9(+^#(*(x, y), minus(y))) } 368.47/210.20 Strict Trs: 368.47/210.20 { +(0(), y) -> y 368.47/210.20 , +(s(x), y) -> s(+(x, y)) 368.47/210.20 , +(p(x), y) -> p(+(x, y)) 368.47/210.20 , minus(0()) -> 0() 368.47/210.20 , minus(s(x)) -> p(minus(x)) 368.47/210.20 , minus(p(x)) -> s(minus(x)) 368.47/210.20 , *(0(), y) -> 0() 368.47/210.20 , *(s(x), y) -> +(*(x, y), y) 368.47/210.20 , *(p(x), y) -> +(*(x, y), minus(y)) } 368.47/210.20 Obligation: 368.47/210.20 runtime complexity 368.47/210.20 Answer: 368.47/210.20 MAYBE 368.47/210.20 368.47/210.20 We estimate the number of application of {4,7} by applications of 368.47/210.20 Pre({4,7}) = {1,5,6}. Here rules are labeled as follows: 368.47/210.20 368.47/210.20 DPs: 368.47/210.20 { 1: +^#(0(), y) -> c_1(y) 368.47/210.20 , 2: +^#(s(x), y) -> c_2(+^#(x, y)) 368.47/210.20 , 3: +^#(p(x), y) -> c_3(+^#(x, y)) 368.47/210.20 , 4: minus^#(0()) -> c_4() 368.47/210.20 , 5: minus^#(s(x)) -> c_5(minus^#(x)) 368.47/210.20 , 6: minus^#(p(x)) -> c_6(minus^#(x)) 368.47/210.20 , 7: *^#(0(), y) -> c_7() 368.47/210.20 , 8: *^#(s(x), y) -> c_8(+^#(*(x, y), y)) 368.47/210.20 , 9: *^#(p(x), y) -> c_9(+^#(*(x, y), minus(y))) } 368.47/210.20 368.47/210.20 We are left with following problem, upon which TcT provides the 368.47/210.20 certificate MAYBE. 368.47/210.20 368.47/210.20 Strict DPs: 368.47/210.20 { +^#(0(), y) -> c_1(y) 368.47/210.20 , +^#(s(x), y) -> c_2(+^#(x, y)) 368.47/210.20 , +^#(p(x), y) -> c_3(+^#(x, y)) 368.47/210.20 , minus^#(s(x)) -> c_5(minus^#(x)) 368.47/210.20 , minus^#(p(x)) -> c_6(minus^#(x)) 368.47/210.20 , *^#(s(x), y) -> c_8(+^#(*(x, y), y)) 368.47/210.20 , *^#(p(x), y) -> c_9(+^#(*(x, y), minus(y))) } 368.47/210.20 Strict Trs: 368.47/210.20 { +(0(), y) -> y 368.47/210.20 , +(s(x), y) -> s(+(x, y)) 368.47/210.20 , +(p(x), y) -> p(+(x, y)) 368.47/210.20 , minus(0()) -> 0() 368.47/210.20 , minus(s(x)) -> p(minus(x)) 368.47/210.20 , minus(p(x)) -> s(minus(x)) 368.47/210.20 , *(0(), y) -> 0() 368.47/210.20 , *(s(x), y) -> +(*(x, y), y) 368.47/210.20 , *(p(x), y) -> +(*(x, y), minus(y)) } 368.47/210.20 Weak DPs: 368.47/210.20 { minus^#(0()) -> c_4() 368.47/210.20 , *^#(0(), y) -> c_7() } 368.47/210.20 Obligation: 368.47/210.20 runtime complexity 368.47/210.20 Answer: 368.47/210.20 MAYBE 368.47/210.20 368.47/210.20 Empty strict component of the problem is NOT empty. 368.47/210.20 368.47/210.20 368.47/210.20 Arrrr.. 368.66/210.41 EOF