YES(O(1),O(n^1)) 16.08/8.63 YES(O(1),O(n^1)) 16.08/8.63 16.08/8.63 We are left with following problem, upon which TcT provides the 16.08/8.63 certificate YES(O(1),O(n^1)). 16.08/8.63 16.08/8.63 Strict Trs: 16.08/8.63 { div(x, y) -> quot(x, y, y) 16.08/8.63 , div(0(), y) -> 0() 16.08/8.63 , quot(x, 0(), s(z)) -> s(div(x, s(z))) 16.08/8.63 , quot(0(), s(y), z) -> 0() 16.08/8.63 , quot(s(x), s(y), z) -> quot(x, y, z) } 16.08/8.63 Obligation: 16.08/8.63 innermost runtime complexity 16.08/8.63 Answer: 16.08/8.63 YES(O(1),O(n^1)) 16.08/8.63 16.08/8.63 We add the following weak dependency pairs: 16.08/8.63 16.08/8.63 Strict DPs: 16.08/8.63 { div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.63 , div^#(0(), y) -> c_2() 16.08/8.63 , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.63 , quot^#(0(), s(y), z) -> c_4() 16.08/8.63 , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.63 16.08/8.63 and mark the set of starting terms. 16.08/8.63 16.08/8.63 We are left with following problem, upon which TcT provides the 16.08/8.63 certificate YES(O(1),O(n^1)). 16.08/8.63 16.08/8.63 Strict DPs: 16.08/8.63 { div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.63 , div^#(0(), y) -> c_2() 16.08/8.63 , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.63 , quot^#(0(), s(y), z) -> c_4() 16.08/8.63 , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.63 Strict Trs: 16.08/8.63 { div(x, y) -> quot(x, y, y) 16.08/8.63 , div(0(), y) -> 0() 16.08/8.68 , quot(x, 0(), s(z)) -> s(div(x, s(z))) 16.08/8.68 , quot(0(), s(y), z) -> 0() 16.08/8.68 , quot(s(x), s(y), z) -> quot(x, y, z) } 16.08/8.68 Obligation: 16.08/8.68 innermost runtime complexity 16.08/8.68 Answer: 16.08/8.68 YES(O(1),O(n^1)) 16.08/8.68 16.08/8.68 No rule is usable, rules are removed from the input problem. 16.08/8.68 16.08/8.68 We are left with following problem, upon which TcT provides the 16.08/8.68 certificate YES(O(1),O(n^1)). 16.08/8.68 16.08/8.68 Strict DPs: 16.08/8.68 { div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.68 , div^#(0(), y) -> c_2() 16.08/8.68 , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.68 , quot^#(0(), s(y), z) -> c_4() 16.08/8.68 , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.68 Obligation: 16.08/8.68 innermost runtime complexity 16.08/8.68 Answer: 16.08/8.68 YES(O(1),O(n^1)) 16.08/8.68 16.08/8.68 The weightgap principle applies (using the following constant 16.08/8.68 growth matrix-interpretation) 16.08/8.68 16.08/8.68 The following argument positions are usable: 16.08/8.68 Uargs(c_1) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1} 16.08/8.68 16.08/8.68 TcT has computed the following constructor-restricted matrix 16.08/8.68 interpretation. 16.08/8.68 16.08/8.68 [0] = [0] 16.08/8.68 [0] 16.08/8.68 16.08/8.68 [s](x1) = [0] 16.08/8.68 [0] 16.08/8.68 16.08/8.68 [div^#](x1, x2) = [1] 16.08/8.68 [0] 16.08/8.68 16.08/8.68 [c_1](x1) = [1 0] x1 + [2] 16.08/8.68 [0 1] [2] 16.08/8.68 16.08/8.68 [quot^#](x1, x2, x3) = [0] 16.08/8.68 [0] 16.08/8.68 16.08/8.68 [c_2] = [0] 16.08/8.68 [0] 16.08/8.68 16.08/8.68 [c_3](x1) = [1 0] x1 + [0] 16.08/8.68 [0 1] [1] 16.08/8.68 16.08/8.68 [c_4] = [1] 16.08/8.68 [0] 16.08/8.68 16.08/8.68 [c_5](x1) = [1 0] x1 + [2] 16.08/8.68 [0 1] [0] 16.08/8.68 16.08/8.68 The order satisfies the following ordering constraints: 16.08/8.68 16.08/8.68 [div^#(x, y)] = [1] 16.08/8.68 [0] 16.08/8.68 ? [2] 16.08/8.68 [2] 16.08/8.68 = [c_1(quot^#(x, y, y))] 16.08/8.68 16.08/8.68 [div^#(0(), y)] = [1] 16.08/8.68 [0] 16.08/8.68 > [0] 16.08/8.68 [0] 16.08/8.68 = [c_2()] 16.08/8.68 16.08/8.68 [quot^#(x, 0(), s(z))] = [0] 16.08/8.68 [0] 16.08/8.68 ? [1] 16.08/8.68 [1] 16.08/8.68 = [c_3(div^#(x, s(z)))] 16.08/8.68 16.08/8.68 [quot^#(0(), s(y), z)] = [0] 16.08/8.68 [0] 16.08/8.68 ? [1] 16.08/8.68 [0] 16.08/8.68 = [c_4()] 16.08/8.68 16.08/8.68 [quot^#(s(x), s(y), z)] = [0] 16.08/8.68 [0] 16.08/8.68 ? [2] 16.08/8.68 [0] 16.08/8.68 = [c_5(quot^#(x, y, z))] 16.08/8.68 16.08/8.68 16.08/8.68 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 16.08/8.68 16.08/8.68 We are left with following problem, upon which TcT provides the 16.08/8.68 certificate YES(O(1),O(n^1)). 16.08/8.68 16.08/8.68 Strict DPs: 16.08/8.68 { div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.68 , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.68 , quot^#(0(), s(y), z) -> c_4() 16.08/8.68 , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.68 Weak DPs: { div^#(0(), y) -> c_2() } 16.08/8.68 Obligation: 16.08/8.68 innermost runtime complexity 16.08/8.68 Answer: 16.08/8.68 YES(O(1),O(n^1)) 16.08/8.68 16.08/8.68 We estimate the number of application of {3} by applications of 16.08/8.68 Pre({3}) = {1,4}. Here rules are labeled as follows: 16.08/8.68 16.08/8.68 DPs: 16.08/8.68 { 1: div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.68 , 2: quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.68 , 3: quot^#(0(), s(y), z) -> c_4() 16.08/8.68 , 4: quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) 16.08/8.68 , 5: div^#(0(), y) -> c_2() } 16.08/8.68 16.08/8.68 We are left with following problem, upon which TcT provides the 16.08/8.68 certificate YES(O(1),O(n^1)). 16.08/8.68 16.08/8.68 Strict DPs: 16.08/8.68 { div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.68 , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.68 , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.68 Weak DPs: 16.08/8.68 { div^#(0(), y) -> c_2() 16.08/8.68 , quot^#(0(), s(y), z) -> c_4() } 16.08/8.68 Obligation: 16.08/8.68 innermost runtime complexity 16.08/8.68 Answer: 16.08/8.68 YES(O(1),O(n^1)) 16.08/8.68 16.08/8.68 The following weak DPs constitute a sub-graph of the DG that is 16.08/8.68 closed under successors. The DPs are removed. 16.08/8.68 16.08/8.68 { div^#(0(), y) -> c_2() 16.08/8.68 , quot^#(0(), s(y), z) -> c_4() } 16.08/8.68 16.08/8.68 We are left with following problem, upon which TcT provides the 16.08/8.68 certificate YES(O(1),O(n^1)). 16.08/8.68 16.08/8.68 Strict DPs: 16.08/8.68 { div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.68 , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.68 , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.68 Obligation: 16.08/8.68 innermost runtime complexity 16.08/8.68 Answer: 16.08/8.68 YES(O(1),O(n^1)) 16.08/8.68 16.08/8.68 We use the processor 'matrix interpretation of dimension 1' to 16.08/8.68 orient following rules strictly. 16.08/8.68 16.08/8.68 DPs: 16.08/8.68 { 3: quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.68 16.08/8.68 Sub-proof: 16.08/8.68 ---------- 16.08/8.68 The following argument positions are usable: 16.08/8.68 Uargs(c_1) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1} 16.08/8.68 16.08/8.68 TcT has computed the following constructor-based matrix 16.08/8.68 interpretation satisfying not(EDA). 16.08/8.68 16.08/8.68 [0] = [7] 16.08/8.68 16.08/8.68 [s](x1) = [1] x1 + [4] 16.08/8.68 16.08/8.68 [div^#](x1, x2) = [2] x1 + [0] 16.08/8.68 16.08/8.68 [c_1](x1) = [1] x1 + [0] 16.08/8.68 16.08/8.68 [quot^#](x1, x2, x3) = [2] x1 + [0] 16.08/8.68 16.08/8.68 [c_3](x1) = [1] x1 + [0] 16.08/8.68 16.08/8.68 [c_5](x1) = [1] x1 + [5] 16.08/8.68 16.08/8.68 The order satisfies the following ordering constraints: 16.08/8.68 16.08/8.68 [div^#(x, y)] = [2] x + [0] 16.08/8.68 >= [2] x + [0] 16.08/8.68 = [c_1(quot^#(x, y, y))] 16.08/8.68 16.08/8.68 [quot^#(x, 0(), s(z))] = [2] x + [0] 16.08/8.68 >= [2] x + [0] 16.08/8.68 = [c_3(div^#(x, s(z)))] 16.08/8.68 16.08/8.68 [quot^#(s(x), s(y), z)] = [2] x + [8] 16.08/8.68 > [2] x + [5] 16.08/8.68 = [c_5(quot^#(x, y, z))] 16.08/8.68 16.08/8.68 16.08/8.68 We return to the main proof. Consider the set of all dependency 16.08/8.68 pairs 16.08/8.68 16.08/8.68 : 16.08/8.68 { 1: div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.68 , 2: quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.68 , 3: quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.68 16.08/8.68 Processor 'matrix interpretation of dimension 1' induces the 16.08/8.68 complexity certificate YES(?,O(n^1)) on application of dependency 16.08/8.68 pairs {3}. These cover all (indirect) predecessors of dependency 16.08/8.68 pairs {1,2,3}, their number of application is equally bounded. The 16.08/8.68 dependency pairs are shifted into the weak component. 16.08/8.68 16.08/8.68 We are left with following problem, upon which TcT provides the 16.08/8.68 certificate YES(O(1),O(1)). 16.08/8.68 16.08/8.68 Weak DPs: 16.08/8.68 { div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.68 , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.68 , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.68 Obligation: 16.08/8.68 innermost runtime complexity 16.08/8.68 Answer: 16.08/8.68 YES(O(1),O(1)) 16.08/8.68 16.08/8.68 The following weak DPs constitute a sub-graph of the DG that is 16.08/8.68 closed under successors. The DPs are removed. 16.08/8.68 16.08/8.68 { div^#(x, y) -> c_1(quot^#(x, y, y)) 16.08/8.68 , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z))) 16.08/8.68 , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) } 16.08/8.68 16.08/8.68 We are left with following problem, upon which TcT provides the 16.08/8.68 certificate YES(O(1),O(1)). 16.08/8.68 16.08/8.68 Rules: Empty 16.08/8.68 Obligation: 16.08/8.68 innermost runtime complexity 16.08/8.68 Answer: 16.08/8.68 YES(O(1),O(1)) 16.08/8.68 16.08/8.68 Empty rules are trivially bounded 16.08/8.68 16.08/8.68 Hurray, we answered YES(O(1),O(n^1)) 16.08/8.68 EOF