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