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