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