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