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