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