YES(O(1),O(n^1)) 0.00/0.21 YES(O(1),O(n^1)) 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(n^1)). 0.00/0.21 0.00/0.21 Strict Trs: 0.00/0.21 { sum(0()) -> 0() 0.00/0.21 , sum(s(x)) -> +(sqr(s(x)), sum(x)) 0.00/0.21 , sum(s(x)) -> +(*(s(x), s(x)), sum(x)) 0.00/0.21 , sqr(x) -> *(x, x) } 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(n^1)) 0.00/0.21 0.00/0.21 We add the following weak dependency pairs: 0.00/0.21 0.00/0.21 Strict DPs: 0.00/0.21 { sum^#(0()) -> c_1() 0.00/0.21 , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_3(sum^#(x)) 0.00/0.21 , sqr^#(x) -> c_4() } 0.00/0.21 0.00/0.21 and mark the set of starting terms. 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(n^1)). 0.00/0.21 0.00/0.21 Strict DPs: 0.00/0.21 { sum^#(0()) -> c_1() 0.00/0.21 , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_3(sum^#(x)) 0.00/0.21 , sqr^#(x) -> c_4() } 0.00/0.21 Strict Trs: 0.00/0.21 { sum(0()) -> 0() 0.00/0.21 , sum(s(x)) -> +(sqr(s(x)), sum(x)) 0.00/0.21 , sum(s(x)) -> +(*(s(x), s(x)), sum(x)) 0.00/0.21 , sqr(x) -> *(x, x) } 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(n^1)) 0.00/0.21 0.00/0.21 No rule is usable, rules are removed from the input problem. 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(n^1)). 0.00/0.21 0.00/0.21 Strict DPs: 0.00/0.21 { sum^#(0()) -> c_1() 0.00/0.21 , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_3(sum^#(x)) 0.00/0.21 , sqr^#(x) -> c_4() } 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(n^1)) 0.00/0.21 0.00/0.21 The weightgap principle applies (using the following constant 0.00/0.21 growth matrix-interpretation) 0.00/0.21 0.00/0.21 The following argument positions are usable: 0.00/0.21 Uargs(c_2) = {1, 2}, Uargs(c_3) = {1} 0.00/0.21 0.00/0.21 TcT has computed the following constructor-restricted matrix 0.00/0.21 interpretation. 0.00/0.21 0.00/0.21 [0] = [0] 0.00/0.21 [0] 0.00/0.21 0.00/0.21 [s](x1) = [0] 0.00/0.21 [0] 0.00/0.21 0.00/0.21 [sum^#](x1) = [0] 0.00/0.21 [0] 0.00/0.21 0.00/0.21 [c_1] = [1] 0.00/0.21 [0] 0.00/0.21 0.00/0.21 [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 0.00/0.21 [0 1] [0 1] [2] 0.00/0.21 0.00/0.21 [sqr^#](x1) = [1] 0.00/0.21 [0] 0.00/0.21 0.00/0.21 [c_3](x1) = [1 0] x1 + [2] 0.00/0.21 [0 1] [0] 0.00/0.21 0.00/0.21 [c_4] = [0] 0.00/0.21 [0] 0.00/0.21 0.00/0.21 The order satisfies the following ordering constraints: 0.00/0.21 0.00/0.21 [sum^#(0())] = [0] 0.00/0.21 [0] 0.00/0.21 ? [1] 0.00/0.21 [0] 0.00/0.21 = [c_1()] 0.00/0.21 0.00/0.21 [sum^#(s(x))] = [0] 0.00/0.21 [0] 0.00/0.21 ? [1] 0.00/0.21 [2] 0.00/0.21 = [c_2(sqr^#(s(x)), sum^#(x))] 0.00/0.21 0.00/0.21 [sum^#(s(x))] = [0] 0.00/0.21 [0] 0.00/0.21 ? [2] 0.00/0.21 [0] 0.00/0.21 = [c_3(sum^#(x))] 0.00/0.21 0.00/0.21 [sqr^#(x)] = [1] 0.00/0.21 [0] 0.00/0.21 > [0] 0.00/0.21 [0] 0.00/0.21 = [c_4()] 0.00/0.21 0.00/0.21 0.00/0.21 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(n^1)). 0.00/0.21 0.00/0.21 Strict DPs: 0.00/0.21 { sum^#(0()) -> c_1() 0.00/0.21 , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_3(sum^#(x)) } 0.00/0.21 Weak DPs: { sqr^#(x) -> c_4() } 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(n^1)) 0.00/0.21 0.00/0.21 We estimate the number of application of {1} by applications of 0.00/0.21 Pre({1}) = {2,3}. Here rules are labeled as follows: 0.00/0.21 0.00/0.21 DPs: 0.00/0.21 { 1: sum^#(0()) -> c_1() 0.00/0.21 , 2: sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x)) 0.00/0.21 , 3: sum^#(s(x)) -> c_3(sum^#(x)) 0.00/0.21 , 4: sqr^#(x) -> c_4() } 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(n^1)). 0.00/0.21 0.00/0.21 Strict DPs: 0.00/0.21 { sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_3(sum^#(x)) } 0.00/0.21 Weak DPs: 0.00/0.21 { sum^#(0()) -> c_1() 0.00/0.21 , sqr^#(x) -> c_4() } 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(n^1)) 0.00/0.21 0.00/0.21 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.21 closed under successors. The DPs are removed. 0.00/0.21 0.00/0.21 { sum^#(0()) -> c_1() 0.00/0.21 , sqr^#(x) -> c_4() } 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(n^1)). 0.00/0.21 0.00/0.21 Strict DPs: 0.00/0.21 { sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_3(sum^#(x)) } 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(n^1)) 0.00/0.21 0.00/0.21 Due to missing edges in the dependency-graph, the right-hand sides 0.00/0.21 of following rules could be simplified: 0.00/0.21 0.00/0.21 { sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x)) } 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(n^1)). 0.00/0.21 0.00/0.21 Strict DPs: 0.00/0.21 { sum^#(s(x)) -> c_1(sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_2(sum^#(x)) } 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(n^1)) 0.00/0.21 0.00/0.21 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 0.00/0.21 to orient following rules strictly. 0.00/0.21 0.00/0.21 DPs: 0.00/0.21 { 1: sum^#(s(x)) -> c_1(sum^#(x)) 0.00/0.21 , 2: sum^#(s(x)) -> c_2(sum^#(x)) } 0.00/0.21 0.00/0.21 Sub-proof: 0.00/0.21 ---------- 0.00/0.21 The input was oriented with the instance of 'Small Polynomial Path 0.00/0.21 Order (PS,1-bounded)' as induced by the safe mapping 0.00/0.21 0.00/0.21 safe(s) = {1}, safe(sum^#) = {}, safe(c_1) = {}, safe(c_2) = {} 0.00/0.21 0.00/0.21 and precedence 0.00/0.21 0.00/0.21 empty . 0.00/0.21 0.00/0.21 Following symbols are considered recursive: 0.00/0.21 0.00/0.21 {sum^#} 0.00/0.21 0.00/0.21 The recursion depth is 1. 0.00/0.21 0.00/0.21 Further, following argument filtering is employed: 0.00/0.21 0.00/0.21 pi(s) = [1], pi(sum^#) = [1], pi(c_1) = [1], pi(c_2) = [1] 0.00/0.21 0.00/0.21 Usable defined function symbols are a subset of: 0.00/0.21 0.00/0.21 {sum^#} 0.00/0.21 0.00/0.21 For your convenience, here are the satisfied ordering constraints: 0.00/0.21 0.00/0.21 pi(sum^#(s(x))) = sum^#(s(; x);) 0.00/0.21 > c_1(sum^#(x;);) 0.00/0.21 = pi(c_1(sum^#(x))) 0.00/0.21 0.00/0.21 pi(sum^#(s(x))) = sum^#(s(; x);) 0.00/0.21 > c_2(sum^#(x;);) 0.00/0.21 = pi(c_2(sum^#(x))) 0.00/0.21 0.00/0.21 0.00/0.21 The strictly oriented rules are moved into the weak component. 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(1)). 0.00/0.21 0.00/0.21 Weak DPs: 0.00/0.21 { sum^#(s(x)) -> c_1(sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_2(sum^#(x)) } 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(1)) 0.00/0.21 0.00/0.21 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.21 closed under successors. The DPs are removed. 0.00/0.21 0.00/0.21 { sum^#(s(x)) -> c_1(sum^#(x)) 0.00/0.21 , sum^#(s(x)) -> c_2(sum^#(x)) } 0.00/0.21 0.00/0.21 We are left with following problem, upon which TcT provides the 0.00/0.21 certificate YES(O(1),O(1)). 0.00/0.21 0.00/0.21 Rules: Empty 0.00/0.21 Obligation: 0.00/0.21 innermost runtime complexity 0.00/0.21 Answer: 0.00/0.21 YES(O(1),O(1)) 0.00/0.21 0.00/0.21 Empty rules are trivially bounded 0.00/0.21 0.00/0.21 Hurray, we answered YES(O(1),O(n^1)) 0.00/0.21 EOF