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