YES(O(1),O(n^1)) 27.21/10.10 YES(O(1),O(n^1)) 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(n^1)). 27.21/10.10 27.21/10.10 Strict Trs: 27.21/10.10 { p(s(x)) -> x 27.21/10.10 , fac(s(x)) -> times(s(x), fac(p(s(x)))) 27.21/10.10 , fac(0()) -> s(0()) } 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(n^1)) 27.21/10.10 27.21/10.10 We add the following weak dependency pairs: 27.21/10.10 27.21/10.10 Strict DPs: 27.21/10.10 { p^#(s(x)) -> c_1() 27.21/10.10 , fac^#(s(x)) -> c_2(fac^#(p(s(x)))) 27.21/10.10 , fac^#(0()) -> c_3() } 27.21/10.10 27.21/10.10 and mark the set of starting terms. 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(n^1)). 27.21/10.10 27.21/10.10 Strict DPs: 27.21/10.10 { p^#(s(x)) -> c_1() 27.21/10.10 , fac^#(s(x)) -> c_2(fac^#(p(s(x)))) 27.21/10.10 , fac^#(0()) -> c_3() } 27.21/10.10 Strict Trs: 27.21/10.10 { p(s(x)) -> x 27.21/10.10 , fac(s(x)) -> times(s(x), fac(p(s(x)))) 27.21/10.10 , fac(0()) -> s(0()) } 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(n^1)) 27.21/10.10 27.21/10.10 We replace rewrite rules by usable rules: 27.21/10.10 27.21/10.10 Strict Usable Rules: { p(s(x)) -> x } 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(n^1)). 27.21/10.10 27.21/10.10 Strict DPs: 27.21/10.10 { p^#(s(x)) -> c_1() 27.21/10.10 , fac^#(s(x)) -> c_2(fac^#(p(s(x)))) 27.21/10.10 , fac^#(0()) -> c_3() } 27.21/10.10 Strict Trs: { p(s(x)) -> x } 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(n^1)) 27.21/10.10 27.21/10.10 The weightgap principle applies (using the following constant 27.21/10.10 growth matrix-interpretation) 27.21/10.10 27.21/10.10 The following argument positions are usable: 27.21/10.10 Uargs(fac^#) = {1}, Uargs(c_2) = {1} 27.21/10.10 27.21/10.10 TcT has computed the following constructor-restricted matrix 27.21/10.10 interpretation. 27.21/10.10 27.21/10.10 [p](x1) = [1 0] x1 + [2] 27.21/10.10 [0 1] [0] 27.21/10.10 27.21/10.10 [s](x1) = [1 0] x1 + [0] 27.21/10.10 [0 1] [0] 27.21/10.10 27.21/10.10 [0] = [0] 27.21/10.10 [0] 27.21/10.10 27.21/10.10 [p^#](x1) = [2 2] x1 + [2] 27.21/10.10 [1 2] [2] 27.21/10.10 27.21/10.10 [c_1] = [1] 27.21/10.10 [1] 27.21/10.10 27.21/10.10 [fac^#](x1) = [2 0] x1 + [0] 27.21/10.10 [0 0] [0] 27.21/10.10 27.21/10.10 [c_2](x1) = [1 0] x1 + [2] 27.21/10.10 [0 1] [2] 27.21/10.10 27.21/10.10 [c_3] = [1] 27.21/10.10 [1] 27.21/10.10 27.21/10.10 The order satisfies the following ordering constraints: 27.21/10.10 27.21/10.10 [p(s(x))] = [1 0] x + [2] 27.21/10.10 [0 1] [0] 27.21/10.10 > [1 0] x + [0] 27.21/10.10 [0 1] [0] 27.21/10.10 = [x] 27.21/10.10 27.21/10.10 [p^#(s(x))] = [2 2] x + [2] 27.21/10.10 [1 2] [2] 27.21/10.10 > [1] 27.21/10.10 [1] 27.21/10.10 = [c_1()] 27.21/10.10 27.21/10.10 [fac^#(s(x))] = [2 0] x + [0] 27.21/10.10 [0 0] [0] 27.21/10.10 ? [2 0] x + [6] 27.21/10.10 [0 0] [2] 27.21/10.10 = [c_2(fac^#(p(s(x))))] 27.21/10.10 27.21/10.10 [fac^#(0())] = [0] 27.21/10.10 [0] 27.21/10.10 ? [1] 27.21/10.10 [1] 27.21/10.10 = [c_3()] 27.21/10.10 27.21/10.10 27.21/10.10 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(n^1)). 27.21/10.10 27.21/10.10 Strict DPs: 27.21/10.10 { fac^#(s(x)) -> c_2(fac^#(p(s(x)))) 27.21/10.10 , fac^#(0()) -> c_3() } 27.21/10.10 Weak DPs: { p^#(s(x)) -> c_1() } 27.21/10.10 Weak Trs: { p(s(x)) -> x } 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(n^1)) 27.21/10.10 27.21/10.10 We estimate the number of application of {2} by applications of 27.21/10.10 Pre({2}) = {1}. Here rules are labeled as follows: 27.21/10.10 27.21/10.10 DPs: 27.21/10.10 { 1: fac^#(s(x)) -> c_2(fac^#(p(s(x)))) 27.21/10.10 , 2: fac^#(0()) -> c_3() 27.21/10.10 , 3: p^#(s(x)) -> c_1() } 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(n^1)). 27.21/10.10 27.21/10.10 Strict DPs: { fac^#(s(x)) -> c_2(fac^#(p(s(x)))) } 27.21/10.10 Weak DPs: 27.21/10.10 { p^#(s(x)) -> c_1() 27.21/10.10 , fac^#(0()) -> c_3() } 27.21/10.10 Weak Trs: { p(s(x)) -> x } 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(n^1)) 27.21/10.10 27.21/10.10 The following weak DPs constitute a sub-graph of the DG that is 27.21/10.10 closed under successors. The DPs are removed. 27.21/10.10 27.21/10.10 { p^#(s(x)) -> c_1() 27.21/10.10 , fac^#(0()) -> c_3() } 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(n^1)). 27.21/10.10 27.21/10.10 Strict DPs: { fac^#(s(x)) -> c_2(fac^#(p(s(x)))) } 27.21/10.10 Weak Trs: { p(s(x)) -> x } 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(n^1)) 27.21/10.10 27.21/10.10 We use the processor 'matrix interpretation of dimension 3' to 27.21/10.10 orient following rules strictly. 27.21/10.10 27.21/10.10 DPs: 27.21/10.10 { 1: fac^#(s(x)) -> c_2(fac^#(p(s(x)))) } 27.21/10.10 27.21/10.10 Sub-proof: 27.21/10.10 ---------- 27.21/10.10 The following argument positions are usable: 27.21/10.10 Uargs(c_2) = {1} 27.21/10.10 27.21/10.10 TcT has computed the following constructor-based matrix 27.21/10.10 interpretation satisfying not(EDA) and not(IDA(1)). 27.21/10.10 27.21/10.10 [0 0 1] [0] 27.21/10.10 [p](x1) = [0 4 0] x1 + [0] 27.21/10.10 [0 1 0] [0] 27.21/10.10 27.21/10.10 [1 0 0] [2] 27.21/10.10 [s](x1) = [0 1 1] x1 + [0] 27.21/10.10 [1 0 0] [0] 27.21/10.10 27.21/10.10 [4 0 0] [0] 27.21/10.10 [fac^#](x1) = [0 0 0] x1 + [4] 27.21/10.10 [0 0 0] [0] 27.21/10.10 27.21/10.10 [1 0 0] [1] 27.21/10.10 [c_2](x1) = [0 0 0] x1 + [3] 27.21/10.10 [0 0 0] [0] 27.21/10.10 27.21/10.10 The order satisfies the following ordering constraints: 27.21/10.10 27.21/10.10 [p(s(x))] = [1 0 0] [0] 27.21/10.10 [0 4 4] x + [0] 27.21/10.10 [0 1 1] [0] 27.21/10.10 >= [1 0 0] [0] 27.21/10.10 [0 1 0] x + [0] 27.21/10.10 [0 0 1] [0] 27.21/10.10 = [x] 27.21/10.10 27.21/10.10 [fac^#(s(x))] = [4 0 0] [8] 27.21/10.10 [0 0 0] x + [4] 27.21/10.10 [0 0 0] [0] 27.21/10.10 > [4 0 0] [1] 27.21/10.10 [0 0 0] x + [3] 27.21/10.10 [0 0 0] [0] 27.21/10.10 = [c_2(fac^#(p(s(x))))] 27.21/10.10 27.21/10.10 27.21/10.10 The strictly oriented rules are moved into the weak component. 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(1)). 27.21/10.10 27.21/10.10 Weak DPs: { fac^#(s(x)) -> c_2(fac^#(p(s(x)))) } 27.21/10.10 Weak Trs: { p(s(x)) -> x } 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(1)) 27.21/10.10 27.21/10.10 The following weak DPs constitute a sub-graph of the DG that is 27.21/10.10 closed under successors. The DPs are removed. 27.21/10.10 27.21/10.10 { fac^#(s(x)) -> c_2(fac^#(p(s(x)))) } 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(1)). 27.21/10.10 27.21/10.10 Weak Trs: { p(s(x)) -> x } 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(1)) 27.21/10.10 27.21/10.10 No rule is usable, rules are removed from the input problem. 27.21/10.10 27.21/10.10 We are left with following problem, upon which TcT provides the 27.21/10.10 certificate YES(O(1),O(1)). 27.21/10.10 27.21/10.10 Rules: Empty 27.21/10.10 Obligation: 27.21/10.10 innermost runtime complexity 27.21/10.10 Answer: 27.21/10.10 YES(O(1),O(1)) 27.21/10.10 27.21/10.10 Empty rules are trivially bounded 27.21/10.10 27.21/10.10 Hurray, we answered YES(O(1),O(n^1)) 27.21/10.14 EOF