MAYBE 318.61/119.36 MAYBE 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate MAYBE. 318.61/119.36 318.61/119.36 Strict Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 MAYBE 318.61/119.36 318.61/119.36 None of the processors succeeded. 318.61/119.36 318.61/119.36 Details of failed attempt(s): 318.61/119.36 ----------------------------- 318.61/119.36 1) 'empty' failed due to the following reason: 318.61/119.36 318.61/119.36 Empty strict component of the problem is NOT empty. 318.61/119.36 318.61/119.36 2) 'Best' failed due to the following reason: 318.61/119.36 318.61/119.36 None of the processors succeeded. 318.61/119.36 318.61/119.36 Details of failed attempt(s): 318.61/119.36 ----------------------------- 318.61/119.36 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 318.61/119.36 following reason: 318.61/119.36 318.61/119.36 We add the following dependency tuples: 318.61/119.36 318.61/119.36 Strict DPs: 318.61/119.36 { +^#(x, 0()) -> c_1() 318.61/119.36 , +^#(0(), x) -> c_2() 318.61/119.36 , +^#(s(x), s(y)) -> c_3(+^#(x, y)) 318.61/119.36 , *^#(x, 0()) -> c_4() 318.61/119.36 , *^#(0(), x) -> c_5() 318.61/119.36 , *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , sum^#(nil()) -> c_7() 318.61/119.36 , sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , prod^#(nil()) -> c_9() 318.61/119.36 , prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 318.61/119.36 and mark the set of starting terms. 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate MAYBE. 318.61/119.36 318.61/119.36 Strict DPs: 318.61/119.36 { +^#(x, 0()) -> c_1() 318.61/119.36 , +^#(0(), x) -> c_2() 318.61/119.36 , +^#(s(x), s(y)) -> c_3(+^#(x, y)) 318.61/119.36 , *^#(x, 0()) -> c_4() 318.61/119.36 , *^#(0(), x) -> c_5() 318.61/119.36 , *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , sum^#(nil()) -> c_7() 318.61/119.36 , sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , prod^#(nil()) -> c_9() 318.61/119.36 , prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 MAYBE 318.61/119.36 318.61/119.36 We estimate the number of application of {1,2,4,5,7,9} by 318.61/119.36 applications of Pre({1,2,4,5,7,9}) = {3,6,8,10}. Here rules are 318.61/119.36 labeled as follows: 318.61/119.36 318.61/119.36 DPs: 318.61/119.36 { 1: +^#(x, 0()) -> c_1() 318.61/119.36 , 2: +^#(0(), x) -> c_2() 318.61/119.36 , 3: +^#(s(x), s(y)) -> c_3(+^#(x, y)) 318.61/119.36 , 4: *^#(x, 0()) -> c_4() 318.61/119.36 , 5: *^#(0(), x) -> c_5() 318.61/119.36 , 6: *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , 7: sum^#(nil()) -> c_7() 318.61/119.36 , 8: sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , 9: prod^#(nil()) -> c_9() 318.61/119.36 , 10: prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate MAYBE. 318.61/119.36 318.61/119.36 Strict DPs: 318.61/119.36 { +^#(s(x), s(y)) -> c_3(+^#(x, y)) 318.61/119.36 , *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 Weak DPs: 318.61/119.36 { +^#(x, 0()) -> c_1() 318.61/119.36 , +^#(0(), x) -> c_2() 318.61/119.36 , *^#(x, 0()) -> c_4() 318.61/119.36 , *^#(0(), x) -> c_5() 318.61/119.36 , sum^#(nil()) -> c_7() 318.61/119.36 , prod^#(nil()) -> c_9() } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 MAYBE 318.61/119.36 318.61/119.36 The following weak DPs constitute a sub-graph of the DG that is 318.61/119.36 closed under successors. The DPs are removed. 318.61/119.36 318.61/119.36 { +^#(x, 0()) -> c_1() 318.61/119.36 , +^#(0(), x) -> c_2() 318.61/119.36 , *^#(x, 0()) -> c_4() 318.61/119.36 , *^#(0(), x) -> c_5() 318.61/119.36 , sum^#(nil()) -> c_7() 318.61/119.36 , prod^#(nil()) -> c_9() } 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate MAYBE. 318.61/119.36 318.61/119.36 Strict DPs: 318.61/119.36 { +^#(s(x), s(y)) -> c_3(+^#(x, y)) 318.61/119.36 , *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 MAYBE 318.61/119.36 318.61/119.36 None of the processors succeeded. 318.61/119.36 318.61/119.36 Details of failed attempt(s): 318.61/119.36 ----------------------------- 318.61/119.36 1) 'empty' failed due to the following reason: 318.61/119.36 318.61/119.36 Empty strict component of the problem is NOT empty. 318.61/119.36 318.61/119.36 2) 'With Problem ...' failed due to the following reason: 318.61/119.36 318.61/119.36 We decompose the input problem according to the dependency graph 318.61/119.36 into the upper component 318.61/119.36 318.61/119.36 { sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 318.61/119.36 and lower component 318.61/119.36 318.61/119.36 { +^#(s(x), s(y)) -> c_3(+^#(x, y)) 318.61/119.36 , *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) } 318.61/119.36 318.61/119.36 Further, following extension rules are added to the lower 318.61/119.36 component. 318.61/119.36 318.61/119.36 { sum^#(cons(x, l)) -> +^#(x, sum(l)) 318.61/119.36 , sum^#(cons(x, l)) -> sum^#(l) 318.61/119.36 , prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 318.61/119.36 TcT solves the upper component with certificate YES(O(1),O(n^1)). 318.61/119.36 318.61/119.36 Sub-proof: 318.61/119.36 ---------- 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate YES(O(1),O(n^1)). 318.61/119.36 318.61/119.36 Strict DPs: 318.61/119.36 { sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 YES(O(1),O(n^1)) 318.61/119.36 318.61/119.36 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 318.61/119.36 to orient following rules strictly. 318.61/119.36 318.61/119.36 DPs: 318.61/119.36 { 1: sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , 2: prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , prod(nil()) -> s(0()) } 318.61/119.36 318.61/119.36 Sub-proof: 318.61/119.36 ---------- 318.61/119.36 The input was oriented with the instance of 'Small Polynomial Path 318.61/119.36 Order (PS,1-bounded)' as induced by the safe mapping 318.61/119.36 318.61/119.36 safe(+) = {1, 2}, safe(0) = {}, safe(s) = {1}, safe(*) = {1}, 318.61/119.36 safe(sum) = {}, safe(nil) = {}, safe(cons) = {1, 2}, 318.61/119.36 safe(prod) = {}, safe(+^#) = {}, safe(*^#) = {}, safe(sum^#) = {}, 318.61/119.36 safe(c_8) = {}, safe(prod^#) = {}, safe(c_10) = {} 318.61/119.36 318.61/119.36 and precedence 318.61/119.36 318.61/119.36 sum > *, prod > +, prod > *, sum^# > +, sum^# > *, prod^# > +, 318.61/119.36 prod^# > *, sum ~ prod, sum^# ~ prod^# . 318.61/119.36 318.61/119.36 Following symbols are considered recursive: 318.61/119.36 318.61/119.36 {sum^#, prod^#} 318.61/119.36 318.61/119.36 The recursion depth is 1. 318.61/119.36 318.61/119.36 Further, following argument filtering is employed: 318.61/119.36 318.61/119.36 pi(+) = [1, 2], pi(0) = [], pi(s) = [], pi(*) = [1, 2], 318.61/119.36 pi(sum) = [], pi(nil) = [], pi(cons) = [2], pi(prod) = [], 318.61/119.36 pi(+^#) = [], pi(*^#) = [], pi(sum^#) = [1], pi(c_8) = [1, 2], 318.61/119.36 pi(prod^#) = [1], pi(c_10) = [1, 2] 318.61/119.36 318.61/119.36 Usable defined function symbols are a subset of: 318.61/119.36 318.61/119.36 {*, +^#, *^#, sum^#, prod^#} 318.61/119.36 318.61/119.36 For your convenience, here are the satisfied ordering constraints: 318.61/119.36 318.61/119.36 pi(sum^#(cons(x, l))) = sum^#(cons(; l);) 318.61/119.36 > c_8(+^#(), sum^#(l;);) 318.61/119.36 = pi(c_8(+^#(x, sum(l)), sum^#(l))) 318.61/119.36 318.61/119.36 pi(prod^#(cons(x, l))) = prod^#(cons(; l);) 318.61/119.36 > c_10(*^#(), prod^#(l;);) 318.61/119.36 = pi(c_10(*^#(x, prod(l)), prod^#(l))) 318.61/119.36 318.61/119.36 pi(*(x, 0())) = *(0(); x) 318.61/119.36 > 0() 318.61/119.36 = pi(0()) 318.61/119.36 318.61/119.36 pi(*(0(), x)) = *(x; 0()) 318.61/119.36 > 0() 318.61/119.36 = pi(0()) 318.61/119.36 318.61/119.36 pi(*(s(x), s(y))) = *(s(); s()) 318.61/119.36 > s() 318.61/119.36 = pi(s(+(*(x, y), +(x, y)))) 318.61/119.36 318.61/119.36 318.61/119.36 The strictly oriented rules are moved into the weak component. 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate YES(O(1),O(1)). 318.61/119.36 318.61/119.36 Weak DPs: 318.61/119.36 { sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 YES(O(1),O(1)) 318.61/119.36 318.61/119.36 The following weak DPs constitute a sub-graph of the DG that is 318.61/119.36 closed under successors. The DPs are removed. 318.61/119.36 318.61/119.36 { sum^#(cons(x, l)) -> c_8(+^#(x, sum(l)), sum^#(l)) 318.61/119.36 , prod^#(cons(x, l)) -> c_10(*^#(x, prod(l)), prod^#(l)) } 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate YES(O(1),O(1)). 318.61/119.36 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 YES(O(1),O(1)) 318.61/119.36 318.61/119.36 No rule is usable, rules are removed from the input problem. 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate YES(O(1),O(1)). 318.61/119.36 318.61/119.36 Rules: Empty 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 YES(O(1),O(1)) 318.61/119.36 318.61/119.36 Empty rules are trivially bounded 318.61/119.36 318.61/119.36 We return to the main proof. 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate MAYBE. 318.61/119.36 318.61/119.36 Strict DPs: 318.61/119.36 { +^#(s(x), s(y)) -> c_3(+^#(x, y)) 318.61/119.36 , *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) } 318.61/119.36 Weak DPs: 318.61/119.36 { sum^#(cons(x, l)) -> +^#(x, sum(l)) 318.61/119.36 , sum^#(cons(x, l)) -> sum^#(l) 318.61/119.36 , prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 MAYBE 318.61/119.36 318.61/119.36 We decompose the input problem according to the dependency graph 318.61/119.36 into the upper component 318.61/119.36 318.61/119.36 { *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , sum^#(cons(x, l)) -> +^#(x, sum(l)) 318.61/119.36 , sum^#(cons(x, l)) -> sum^#(l) 318.61/119.36 , prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 318.61/119.36 and lower component 318.61/119.36 318.61/119.36 { +^#(s(x), s(y)) -> c_3(+^#(x, y)) } 318.61/119.36 318.61/119.36 Further, following extension rules are added to the lower 318.61/119.36 component. 318.61/119.36 318.61/119.36 { *^#(s(x), s(y)) -> +^#(x, y) 318.61/119.36 , *^#(s(x), s(y)) -> +^#(*(x, y), +(x, y)) 318.61/119.36 , *^#(s(x), s(y)) -> *^#(x, y) 318.61/119.36 , sum^#(cons(x, l)) -> +^#(x, sum(l)) 318.61/119.36 , sum^#(cons(x, l)) -> sum^#(l) 318.61/119.36 , prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 318.61/119.36 TcT solves the upper component with certificate YES(O(1),O(n^1)). 318.61/119.36 318.61/119.36 Sub-proof: 318.61/119.36 ---------- 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate YES(O(1),O(n^1)). 318.61/119.36 318.61/119.36 Strict DPs: 318.61/119.36 { *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , sum^#(cons(x, l)) -> +^#(x, sum(l)) } 318.61/119.36 Weak DPs: 318.61/119.36 { sum^#(cons(x, l)) -> sum^#(l) 318.61/119.36 , prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 YES(O(1),O(n^1)) 318.61/119.36 318.61/119.36 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 318.61/119.36 to orient following rules strictly. 318.61/119.36 318.61/119.36 DPs: 318.61/119.36 { 1: *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , 2: sum^#(cons(x, l)) -> +^#(x, sum(l)) 318.61/119.36 , 4: prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , 5: prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 Trs: 318.61/119.36 { +(0(), x) -> x 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , prod(nil()) -> s(0()) } 318.61/119.36 318.61/119.36 Sub-proof: 318.61/119.36 ---------- 318.61/119.36 The input was oriented with the instance of 'Small Polynomial Path 318.61/119.36 Order (PS,1-bounded)' as induced by the safe mapping 318.61/119.36 318.61/119.36 safe(+) = {}, safe(0) = {}, safe(s) = {1}, safe(*) = {}, 318.61/119.36 safe(sum) = {}, safe(nil) = {}, safe(cons) = {1, 2}, 318.61/119.36 safe(prod) = {}, safe(+^#) = {}, safe(*^#) = {2}, safe(c_6) = {}, 318.61/119.36 safe(sum^#) = {}, safe(prod^#) = {} 318.61/119.36 318.61/119.36 and precedence 318.61/119.36 318.61/119.36 * > +, * > prod, sum > +, sum > *, sum > prod, *^# > +, *^# > prod, 318.61/119.36 sum^# > +, sum^# > *, sum^# > prod, prod^# > +, + ~ prod, 318.61/119.36 sum ~ sum^#, *^# ~ prod^# . 318.61/119.36 318.61/119.36 Following symbols are considered recursive: 318.61/119.36 318.61/119.36 {*^#, prod^#} 318.61/119.36 318.61/119.36 The recursion depth is 1. 318.61/119.36 318.61/119.36 Further, following argument filtering is employed: 318.61/119.36 318.61/119.36 pi(+) = [2], pi(0) = [], pi(s) = [1], pi(*) = [], pi(sum) = [], 318.61/119.36 pi(nil) = [], pi(cons) = [1, 2], pi(prod) = [], pi(+^#) = [], 318.61/119.36 pi(*^#) = [1], pi(c_6) = [1, 2, 3], pi(sum^#) = [], 318.61/119.36 pi(prod^#) = [1] 318.61/119.36 318.61/119.36 Usable defined function symbols are a subset of: 318.61/119.36 318.61/119.36 {+^#, *^#, sum^#, prod^#} 318.61/119.36 318.61/119.36 For your convenience, here are the satisfied ordering constraints: 318.61/119.36 318.61/119.36 pi(*^#(s(x), s(y))) = *^#(s(; x);) 318.61/119.36 > c_6(+^#(), *^#(x;), +^#();) 318.61/119.36 = pi(c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y))) 318.61/119.36 318.61/119.36 pi(sum^#(cons(x, l))) = sum^#() 318.61/119.36 > +^#() 318.61/119.36 = pi(+^#(x, sum(l))) 318.61/119.36 318.61/119.36 pi(sum^#(cons(x, l))) = sum^#() 318.61/119.36 >= sum^#() 318.61/119.36 = pi(sum^#(l)) 318.61/119.36 318.61/119.36 pi(prod^#(cons(x, l))) = prod^#(cons(; x, l);) 318.61/119.36 > *^#(x;) 318.61/119.36 = pi(*^#(x, prod(l))) 318.61/119.36 318.61/119.36 pi(prod^#(cons(x, l))) = prod^#(cons(; x, l);) 318.61/119.36 > prod^#(l;) 318.61/119.36 = pi(prod^#(l)) 318.61/119.36 318.61/119.36 318.61/119.36 The strictly oriented rules are moved into the weak component. 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate YES(O(1),O(1)). 318.61/119.36 318.61/119.36 Weak DPs: 318.61/119.36 { *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , sum^#(cons(x, l)) -> +^#(x, sum(l)) 318.61/119.36 , sum^#(cons(x, l)) -> sum^#(l) 318.61/119.36 , prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 YES(O(1),O(1)) 318.61/119.36 318.61/119.36 The following weak DPs constitute a sub-graph of the DG that is 318.61/119.36 closed under successors. The DPs are removed. 318.61/119.36 318.61/119.36 { *^#(s(x), s(y)) -> 318.61/119.36 c_6(+^#(*(x, y), +(x, y)), *^#(x, y), +^#(x, y)) 318.61/119.36 , sum^#(cons(x, l)) -> +^#(x, sum(l)) 318.61/119.36 , sum^#(cons(x, l)) -> sum^#(l) 318.61/119.36 , prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate YES(O(1),O(1)). 318.61/119.36 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 YES(O(1),O(1)) 318.61/119.36 318.61/119.36 No rule is usable, rules are removed from the input problem. 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate YES(O(1),O(1)). 318.61/119.36 318.61/119.36 Rules: Empty 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 YES(O(1),O(1)) 318.61/119.36 318.61/119.36 Empty rules are trivially bounded 318.61/119.36 318.61/119.36 We return to the main proof. 318.61/119.36 318.61/119.36 We are left with following problem, upon which TcT provides the 318.61/119.36 certificate MAYBE. 318.61/119.36 318.61/119.36 Strict DPs: { +^#(s(x), s(y)) -> c_3(+^#(x, y)) } 318.61/119.36 Weak DPs: 318.61/119.36 { *^#(s(x), s(y)) -> +^#(x, y) 318.61/119.36 , *^#(s(x), s(y)) -> +^#(*(x, y), +(x, y)) 318.61/119.36 , *^#(s(x), s(y)) -> *^#(x, y) 318.61/119.36 , sum^#(cons(x, l)) -> +^#(x, sum(l)) 318.61/119.36 , sum^#(cons(x, l)) -> sum^#(l) 318.61/119.36 , prod^#(cons(x, l)) -> *^#(x, prod(l)) 318.61/119.36 , prod^#(cons(x, l)) -> prod^#(l) } 318.61/119.36 Weak Trs: 318.61/119.36 { +(x, 0()) -> x 318.61/119.36 , +(0(), x) -> x 318.61/119.36 , +(s(x), s(y)) -> s(s(+(x, y))) 318.61/119.36 , *(x, 0()) -> 0() 318.61/119.36 , *(0(), x) -> 0() 318.61/119.36 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 318.61/119.36 , sum(nil()) -> 0() 318.61/119.36 , sum(cons(x, l)) -> +(x, sum(l)) 318.61/119.36 , prod(nil()) -> s(0()) 318.61/119.36 , prod(cons(x, l)) -> *(x, prod(l)) } 318.61/119.36 Obligation: 318.61/119.36 innermost runtime complexity 318.61/119.36 Answer: 318.61/119.36 MAYBE 318.61/119.36 318.61/119.36 None of the processors succeeded. 318.61/119.36 318.61/119.36 Details of failed attempt(s): 318.61/119.36 ----------------------------- 318.61/119.36 1) 'empty' failed due to the following reason: 318.61/119.36 318.61/119.36 Empty strict component of the problem is NOT empty. 318.61/119.36 318.61/119.36 2) 'Fastest' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'With Problem ...' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'empty' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 2) 'Polynomial Path Order (PS)' failed due to the following reason: 318.61/119.37 318.61/119.37 The input cannot be shown compatible 318.61/119.37 318.61/119.37 318.61/119.37 2) 'Polynomial Path Order (PS)' failed due to the following reason: 318.61/119.37 318.61/119.37 The input cannot be shown compatible 318.61/119.37 318.61/119.37 3) 'Fastest (timeout of 24 seconds)' failed due to the following 318.61/119.37 reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 318.61/119.37 failed due to the following reason: 318.61/119.37 318.61/119.37 match-boundness of the problem could not be verified. 318.61/119.37 318.61/119.37 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 318.61/119.37 failed due to the following reason: 318.61/119.37 318.61/119.37 match-boundness of the problem could not be verified. 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 2) 'Best' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 318.61/119.37 seconds)' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'empty' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 2) 'With Problem ...' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'empty' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 2) 'Fastest' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'With Problem ...' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'empty' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 2) 'With Problem ...' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 318.61/119.37 2) 'With Problem ...' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'empty' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 2) 'With Problem ...' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'empty' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 2) 'With Problem ...' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'empty' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 2) 'With Problem ...' failed due to the following reason: 318.61/119.37 318.61/119.37 Empty strict component of the problem is NOT empty. 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 2) 'Best' failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 318.61/119.37 following reason: 318.61/119.37 318.61/119.37 The input cannot be shown compatible 318.61/119.37 318.61/119.37 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 318.61/119.37 to the following reason: 318.61/119.37 318.61/119.37 The input cannot be shown compatible 318.61/119.37 318.61/119.37 318.61/119.37 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 318.61/119.37 failed due to the following reason: 318.61/119.37 318.61/119.37 None of the processors succeeded. 318.61/119.37 318.61/119.37 Details of failed attempt(s): 318.61/119.37 ----------------------------- 318.61/119.37 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 318.61/119.37 failed due to the following reason: 318.61/119.37 318.61/119.37 match-boundness of the problem could not be verified. 318.61/119.37 318.61/119.37 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 318.61/119.37 failed due to the following reason: 318.61/119.37 318.61/119.37 match-boundness of the problem could not be verified. 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 318.61/119.37 Arrrr.. 318.61/119.37 EOF