YES(O(1),O(n^3)) 367.07/96.57 YES(O(1),O(n^3)) 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(n^3)). 367.07/96.57 367.07/96.57 Strict Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) 367.07/96.57 , quot(0(), s(Y)) -> 0() 367.07/96.57 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(n^3)) 367.07/96.57 367.07/96.57 We add the following dependency tuples: 367.07/96.57 367.07/96.57 Strict DPs: 367.07/96.57 { le^#(0(), Y) -> c_1() 367.07/96.57 , le^#(s(X), 0()) -> c_2() 367.07/96.57 , le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(0(), Y) -> c_4() 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(true(), s(X), Y) -> c_6() 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , quot^#(0(), s(Y)) -> c_8() 367.07/96.57 , quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 367.07/96.57 and mark the set of starting terms. 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(n^3)). 367.07/96.57 367.07/96.57 Strict DPs: 367.07/96.57 { le^#(0(), Y) -> c_1() 367.07/96.57 , le^#(s(X), 0()) -> c_2() 367.07/96.57 , le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(0(), Y) -> c_4() 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(true(), s(X), Y) -> c_6() 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , quot^#(0(), s(Y)) -> c_8() 367.07/96.57 , quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) 367.07/96.57 , quot(0(), s(Y)) -> 0() 367.07/96.57 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(n^3)) 367.07/96.57 367.07/96.57 We estimate the number of application of {1,2,4,6,8} by 367.07/96.57 applications of Pre({1,2,4,6,8}) = {3,5,7,9}. Here rules are 367.07/96.57 labeled as follows: 367.07/96.57 367.07/96.57 DPs: 367.07/96.57 { 1: le^#(0(), Y) -> c_1() 367.07/96.57 , 2: le^#(s(X), 0()) -> c_2() 367.07/96.57 , 3: le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , 4: minus^#(0(), Y) -> c_4() 367.07/96.57 , 5: minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , 6: ifMinus^#(true(), s(X), Y) -> c_6() 367.07/96.57 , 7: ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , 8: quot^#(0(), s(Y)) -> c_8() 367.07/96.57 , 9: quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(n^3)). 367.07/96.57 367.07/96.57 Strict DPs: 367.07/96.57 { le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 Weak DPs: 367.07/96.57 { le^#(0(), Y) -> c_1() 367.07/96.57 , le^#(s(X), 0()) -> c_2() 367.07/96.57 , minus^#(0(), Y) -> c_4() 367.07/96.57 , ifMinus^#(true(), s(X), Y) -> c_6() 367.07/96.57 , quot^#(0(), s(Y)) -> c_8() } 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) 367.07/96.57 , quot(0(), s(Y)) -> 0() 367.07/96.57 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(n^3)) 367.07/96.57 367.07/96.57 The following weak DPs constitute a sub-graph of the DG that is 367.07/96.57 closed under successors. The DPs are removed. 367.07/96.57 367.07/96.57 { le^#(0(), Y) -> c_1() 367.07/96.57 , le^#(s(X), 0()) -> c_2() 367.07/96.57 , minus^#(0(), Y) -> c_4() 367.07/96.57 , ifMinus^#(true(), s(X), Y) -> c_6() 367.07/96.57 , quot^#(0(), s(Y)) -> c_8() } 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(n^3)). 367.07/96.57 367.07/96.57 Strict DPs: 367.07/96.57 { le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) 367.07/96.57 , quot(0(), s(Y)) -> 0() 367.07/96.57 , quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(n^3)) 367.07/96.57 367.07/96.57 We replace rewrite rules by usable rules: 367.07/96.57 367.07/96.57 Weak Usable Rules: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(n^3)). 367.07/96.57 367.07/96.57 Strict DPs: 367.07/96.57 { le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(n^3)) 367.07/96.57 367.07/96.57 We decompose the input problem according to the dependency graph 367.07/96.57 into the upper component 367.07/96.57 367.07/96.57 { quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 367.07/96.57 and lower component 367.07/96.57 367.07/96.57 { le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) } 367.07/96.57 367.07/96.57 Further, following extension rules are added to the lower 367.07/96.57 component. 367.07/96.57 367.07/96.57 { quot^#(s(X), s(Y)) -> minus^#(X, Y) 367.07/96.57 , quot^#(s(X), s(Y)) -> quot^#(minus(X, Y), s(Y)) } 367.07/96.57 367.07/96.57 TcT solves the upper component with certificate YES(O(1),O(n^1)). 367.07/96.57 367.07/96.57 Sub-proof: 367.07/96.57 ---------- 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(n^1)). 367.07/96.57 367.07/96.57 Strict DPs: 367.07/96.57 { quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(n^1)) 367.07/96.57 367.07/96.57 We use the processor 'matrix interpretation of dimension 1' to 367.07/96.57 orient following rules strictly. 367.07/96.57 367.07/96.57 DPs: 367.07/96.57 { 1: quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 Trs: { ifMinus(true(), s(X), Y) -> 0() } 367.07/96.57 367.07/96.57 Sub-proof: 367.07/96.57 ---------- 367.07/96.57 The following argument positions are usable: 367.07/96.57 Uargs(c_9) = {1} 367.07/96.57 367.07/96.57 TcT has computed the following constructor-based matrix 367.07/96.57 interpretation satisfying not(EDA). 367.07/96.57 367.07/96.57 [le](x1, x2) = [0] 367.07/96.57 367.07/96.57 [0] = [0] 367.07/96.57 367.07/96.57 [true] = [0] 367.07/96.57 367.07/96.57 [s](x1) = [1] x1 + [1] 367.07/96.57 367.07/96.57 [false] = [0] 367.07/96.57 367.07/96.57 [minus](x1, x2) = [1] x1 + [0] 367.07/96.57 367.07/96.57 [ifMinus](x1, x2, x3) = [1] x2 + [0] 367.07/96.57 367.07/96.57 [minus^#](x1, x2) = [7] x1 + [7] x2 + [7] 367.07/96.57 367.07/96.57 [quot^#](x1, x2) = [1] x1 + [0] 367.07/96.57 367.07/96.57 [c_9](x1, x2) = [1] x1 + [0] 367.07/96.57 367.07/96.57 The order satisfies the following ordering constraints: 367.07/96.57 367.07/96.57 [le(0(), Y)] = [0] 367.07/96.57 >= [0] 367.07/96.57 = [true()] 367.07/96.57 367.07/96.57 [le(s(X), 0())] = [0] 367.07/96.57 >= [0] 367.07/96.57 = [false()] 367.07/96.57 367.07/96.57 [le(s(X), s(Y))] = [0] 367.07/96.57 >= [0] 367.07/96.57 = [le(X, Y)] 367.07/96.57 367.07/96.57 [minus(0(), Y)] = [0] 367.07/96.57 >= [0] 367.07/96.57 = [0()] 367.07/96.57 367.07/96.57 [minus(s(X), Y)] = [1] X + [1] 367.07/96.57 >= [1] X + [1] 367.07/96.57 = [ifMinus(le(s(X), Y), s(X), Y)] 367.07/96.57 367.07/96.57 [ifMinus(true(), s(X), Y)] = [1] X + [1] 367.07/96.57 > [0] 367.07/96.57 = [0()] 367.07/96.57 367.07/96.57 [ifMinus(false(), s(X), Y)] = [1] X + [1] 367.07/96.57 >= [1] X + [1] 367.07/96.57 = [s(minus(X, Y))] 367.07/96.57 367.07/96.57 [quot^#(s(X), s(Y))] = [1] X + [1] 367.07/96.57 > [1] X + [0] 367.07/96.57 = [c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y))] 367.07/96.57 367.07/96.57 367.07/96.57 The strictly oriented rules are moved into the weak component. 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(1)). 367.07/96.57 367.07/96.57 Weak DPs: 367.07/96.57 { quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(1)) 367.07/96.57 367.07/96.57 The following weak DPs constitute a sub-graph of the DG that is 367.07/96.57 closed under successors. The DPs are removed. 367.07/96.57 367.07/96.57 { quot^#(s(X), s(Y)) -> 367.07/96.57 c_9(quot^#(minus(X, Y), s(Y)), minus^#(X, Y)) } 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(1)). 367.07/96.57 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(1)) 367.07/96.57 367.07/96.57 No rule is usable, rules are removed from the input problem. 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(1)). 367.07/96.57 367.07/96.57 Rules: Empty 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(1)) 367.07/96.57 367.07/96.57 Empty rules are trivially bounded 367.07/96.57 367.07/96.57 We return to the main proof. 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(n^2)). 367.07/96.57 367.07/96.57 Strict DPs: 367.07/96.57 { le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) } 367.07/96.57 Weak DPs: 367.07/96.57 { quot^#(s(X), s(Y)) -> minus^#(X, Y) 367.07/96.57 , quot^#(s(X), s(Y)) -> quot^#(minus(X, Y), s(Y)) } 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(n^2)) 367.07/96.57 367.07/96.57 We use the processor 'matrix interpretation of dimension 2' to 367.07/96.57 orient following rules strictly. 367.07/96.57 367.07/96.57 DPs: 367.07/96.57 { 1: le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , 2: minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) } 367.07/96.57 Trs: 367.07/96.57 { ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 367.07/96.57 Sub-proof: 367.07/96.57 ---------- 367.07/96.57 The following argument positions are usable: 367.07/96.57 Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, Uargs(c_7) = {1} 367.07/96.57 367.07/96.57 TcT has computed the following constructor-based matrix 367.07/96.57 interpretation satisfying not(EDA). 367.07/96.57 367.07/96.57 [le](x1, x2) = [0] 367.07/96.57 [0] 367.07/96.57 367.07/96.57 [0] = [0] 367.07/96.57 [0] 367.07/96.57 367.07/96.57 [true] = [0] 367.07/96.57 [0] 367.07/96.57 367.07/96.57 [s](x1) = [1 4] x1 + [0] 367.07/96.57 [0 1] [2] 367.07/96.57 367.07/96.57 [false] = [0] 367.07/96.57 [0] 367.07/96.57 367.07/96.57 [minus](x1, x2) = [1 4] x1 + [0] 367.07/96.57 [0 1] [0] 367.07/96.57 367.07/96.57 [ifMinus](x1, x2, x3) = [1 4] x2 + [0] 367.07/96.57 [0 1] [0] 367.07/96.57 367.07/96.57 [le^#](x1, x2) = [0 1] x1 + [0] 367.07/96.57 [0 4] [0] 367.07/96.57 367.07/96.57 [c_3](x1) = [1 0] x1 + [1] 367.07/96.57 [0 0] [3] 367.07/96.57 367.07/96.57 [minus^#](x1, x2) = [2 4] x1 + [0] 367.07/96.57 [0 0] [4] 367.07/96.57 367.07/96.57 [c_5](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 367.07/96.57 [0 0] [0 0] [3] 367.07/96.57 367.07/96.57 [ifMinus^#](x1, x2, x3) = [2 0] x2 + [0 0] x3 + [0] 367.07/96.57 [2 0] [4 0] [4] 367.07/96.57 367.07/96.57 [c_7](x1) = [1 0] x1 + [0] 367.07/96.57 [0 0] [3] 367.07/96.57 367.07/96.57 [quot^#](x1, x2) = [2 0] x1 + [0] 367.07/96.57 [0 4] [0] 367.07/96.57 367.07/96.57 The order satisfies the following ordering constraints: 367.07/96.57 367.07/96.57 [le(0(), Y)] = [0] 367.07/96.57 [0] 367.07/96.57 >= [0] 367.07/96.57 [0] 367.07/96.57 = [true()] 367.07/96.57 367.07/96.57 [le(s(X), 0())] = [0] 367.07/96.57 [0] 367.07/96.57 >= [0] 367.07/96.57 [0] 367.07/96.57 = [false()] 367.07/96.57 367.07/96.57 [le(s(X), s(Y))] = [0] 367.07/96.57 [0] 367.07/96.57 >= [0] 367.07/96.57 [0] 367.07/96.57 = [le(X, Y)] 367.07/96.57 367.07/96.57 [minus(0(), Y)] = [0] 367.07/96.57 [0] 367.07/96.57 >= [0] 367.07/96.57 [0] 367.07/96.57 = [0()] 367.07/96.57 367.07/96.57 [minus(s(X), Y)] = [1 8] X + [8] 367.07/96.57 [0 1] [2] 367.07/96.57 >= [1 8] X + [8] 367.07/96.57 [0 1] [2] 367.07/96.57 = [ifMinus(le(s(X), Y), s(X), Y)] 367.07/96.57 367.07/96.57 [ifMinus(true(), s(X), Y)] = [1 8] X + [8] 367.07/96.57 [0 1] [2] 367.07/96.57 > [0] 367.07/96.57 [0] 367.07/96.57 = [0()] 367.07/96.57 367.07/96.57 [ifMinus(false(), s(X), Y)] = [1 8] X + [8] 367.07/96.57 [0 1] [2] 367.07/96.57 > [1 8] X + [0] 367.07/96.57 [0 1] [2] 367.07/96.57 = [s(minus(X, Y))] 367.07/96.57 367.07/96.57 [le^#(s(X), s(Y))] = [0 1] X + [2] 367.07/96.57 [0 4] [8] 367.07/96.57 > [0 1] X + [1] 367.07/96.57 [0 0] [3] 367.07/96.57 = [c_3(le^#(X, Y))] 367.07/96.57 367.07/96.57 [minus^#(s(X), Y)] = [2 12] X + [8] 367.07/96.57 [0 0] [4] 367.07/96.57 > [2 9] X + [3] 367.07/96.57 [0 0] [3] 367.07/96.57 = [c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y))] 367.07/96.57 367.07/96.57 [ifMinus^#(false(), s(X), Y)] = [0 0] Y + [2 8] X + [0] 367.07/96.57 [4 0] [2 8] [4] 367.07/96.57 >= [2 4] X + [0] 367.07/96.57 [0 0] [3] 367.07/96.57 = [c_7(minus^#(X, Y))] 367.07/96.57 367.07/96.57 [quot^#(s(X), s(Y))] = [2 8] X + [0] 367.07/96.57 [0 4] [8] 367.07/96.57 >= [2 4] X + [0] 367.07/96.57 [0 0] [4] 367.07/96.57 = [minus^#(X, Y)] 367.07/96.57 367.07/96.57 [quot^#(s(X), s(Y))] = [2 8] X + [0] 367.07/96.57 [0 4] [8] 367.07/96.57 >= [2 8] X + [0] 367.07/96.57 [0 4] [0] 367.07/96.57 = [quot^#(minus(X, Y), s(Y))] 367.07/96.57 367.07/96.57 367.07/96.57 We return to the main proof. Consider the set of all dependency 367.07/96.57 pairs 367.07/96.57 367.07/96.57 : 367.07/96.57 { 1: le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , 2: minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , 3: ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , 4: quot^#(s(X), s(Y)) -> minus^#(X, Y) 367.07/96.57 , 5: quot^#(s(X), s(Y)) -> quot^#(minus(X, Y), s(Y)) } 367.07/96.57 367.07/96.57 Processor 'matrix interpretation of dimension 2' induces the 367.07/96.57 complexity certificate YES(?,O(n^2)) on application of dependency 367.07/96.57 pairs {1,2}. These cover all (indirect) predecessors of dependency 367.07/96.57 pairs {1,2,3}, their number of application is equally bounded. The 367.07/96.57 dependency pairs are shifted into the weak component. 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(1)). 367.07/96.57 367.07/96.57 Weak DPs: 367.07/96.57 { le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , quot^#(s(X), s(Y)) -> minus^#(X, Y) 367.07/96.57 , quot^#(s(X), s(Y)) -> quot^#(minus(X, Y), s(Y)) } 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(1)) 367.07/96.57 367.07/96.57 The following weak DPs constitute a sub-graph of the DG that is 367.07/96.57 closed under successors. The DPs are removed. 367.07/96.57 367.07/96.57 { le^#(s(X), s(Y)) -> c_3(le^#(X, Y)) 367.07/96.57 , minus^#(s(X), Y) -> 367.07/96.57 c_5(ifMinus^#(le(s(X), Y), s(X), Y), le^#(s(X), Y)) 367.07/96.57 , ifMinus^#(false(), s(X), Y) -> c_7(minus^#(X, Y)) 367.07/96.57 , quot^#(s(X), s(Y)) -> minus^#(X, Y) 367.07/96.57 , quot^#(s(X), s(Y)) -> quot^#(minus(X, Y), s(Y)) } 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(1)). 367.07/96.57 367.07/96.57 Weak Trs: 367.07/96.57 { le(0(), Y) -> true() 367.07/96.57 , le(s(X), 0()) -> false() 367.07/96.57 , le(s(X), s(Y)) -> le(X, Y) 367.07/96.57 , minus(0(), Y) -> 0() 367.07/96.57 , minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y) 367.07/96.57 , ifMinus(true(), s(X), Y) -> 0() 367.07/96.57 , ifMinus(false(), s(X), Y) -> s(minus(X, Y)) } 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(1)) 367.07/96.57 367.07/96.57 No rule is usable, rules are removed from the input problem. 367.07/96.57 367.07/96.57 We are left with following problem, upon which TcT provides the 367.07/96.57 certificate YES(O(1),O(1)). 367.07/96.57 367.07/96.57 Rules: Empty 367.07/96.57 Obligation: 367.07/96.57 innermost runtime complexity 367.07/96.57 Answer: 367.07/96.57 YES(O(1),O(1)) 367.07/96.57 367.07/96.57 Empty rules are trivially bounded 367.07/96.57 367.07/96.57 Hurray, we answered YES(O(1),O(n^3)) 367.07/96.58 EOF