YES(O(1),O(n^1)) 0.00/0.56 YES(O(1),O(n^1)) 0.00/0.56 0.00/0.56 We are left with following problem, upon which TcT provides the 0.00/0.56 certificate YES(O(1),O(n^1)). 0.00/0.56 0.00/0.56 Strict Trs: 0.00/0.56 { gcd(x, 0()) -> x 0.00/0.56 , gcd(0(), y) -> y 0.00/0.56 , gcd(s(x), s(y)) -> 0.00/0.56 if(<(x, y), gcd(s(x), -(y, x)), gcd(-(x, y), s(y))) } 0.00/0.56 Obligation: 0.00/0.56 runtime complexity 0.00/0.56 Answer: 0.00/0.56 YES(O(1),O(n^1)) 0.00/0.56 0.00/0.56 We add the following weak dependency pairs: 0.00/0.56 0.00/0.56 Strict DPs: 0.00/0.56 { gcd^#(x, 0()) -> c_1(x) 0.00/0.56 , gcd^#(0(), y) -> c_2(y) 0.00/0.56 , gcd^#(s(x), s(y)) -> 0.00/0.56 c_3(x, y, gcd^#(s(x), -(y, x)), gcd^#(-(x, y), s(y))) } 0.00/0.56 0.00/0.56 and mark the set of starting terms. 0.00/0.56 0.00/0.56 We are left with following problem, upon which TcT provides the 0.00/0.56 certificate YES(O(1),O(n^1)). 0.00/0.56 0.00/0.56 Strict DPs: 0.00/0.56 { gcd^#(x, 0()) -> c_1(x) 0.00/0.56 , gcd^#(0(), y) -> c_2(y) 0.00/0.56 , gcd^#(s(x), s(y)) -> 0.00/0.56 c_3(x, y, gcd^#(s(x), -(y, x)), gcd^#(-(x, y), s(y))) } 0.00/0.56 Strict Trs: 0.00/0.56 { gcd(x, 0()) -> x 0.00/0.56 , gcd(0(), y) -> y 0.00/0.56 , gcd(s(x), s(y)) -> 0.00/0.56 if(<(x, y), gcd(s(x), -(y, x)), gcd(-(x, y), s(y))) } 0.00/0.56 Obligation: 0.00/0.56 runtime complexity 0.00/0.56 Answer: 0.00/0.56 YES(O(1),O(n^1)) 0.00/0.56 0.00/0.56 No rule is usable, rules are removed from the input problem. 0.00/0.56 0.00/0.56 We are left with following problem, upon which TcT provides the 0.00/0.56 certificate YES(O(1),O(n^1)). 0.00/0.56 0.00/0.56 Strict DPs: 0.00/0.56 { gcd^#(x, 0()) -> c_1(x) 0.00/0.56 , gcd^#(0(), y) -> c_2(y) 0.00/0.56 , gcd^#(s(x), s(y)) -> 0.00/0.56 c_3(x, y, gcd^#(s(x), -(y, x)), gcd^#(-(x, y), s(y))) } 0.00/0.56 Obligation: 0.00/0.56 runtime complexity 0.00/0.56 Answer: 0.00/0.56 YES(O(1),O(n^1)) 0.00/0.56 0.00/0.56 The weightgap principle applies (using the following constant 0.00/0.56 growth matrix-interpretation) 0.00/0.56 0.00/0.56 The following argument positions are usable: 0.00/0.56 none 0.00/0.56 0.00/0.56 TcT has computed the following constructor-restricted matrix 0.00/0.56 interpretation. 0.00/0.56 0.00/0.56 [0] = [0] 0.00/0.56 [0] 0.00/0.56 0.00/0.56 [s](x1) = [0] 0.00/0.56 [2] 0.00/0.56 0.00/0.56 [-](x1, x2) = [0] 0.00/0.56 [0] 0.00/0.56 0.00/0.56 [gcd^#](x1, x2) = [0 2] x1 + [0] 0.00/0.56 [0 0] [0] 0.00/0.56 0.00/0.56 [c_1](x1) = [0 1] x1 + [1] 0.00/0.56 [0 0] [0] 0.00/0.56 0.00/0.56 [c_2](x1) = [1] 0.00/0.56 [0] 0.00/0.56 0.00/0.56 [c_3](x1, x2, x3, x4) = [1] 0.00/0.56 [0] 0.00/0.56 0.00/0.56 The order satisfies the following ordering constraints: 0.00/0.56 0.00/0.56 [gcd^#(x, 0())] = [0 2] x + [0] 0.00/0.56 [0 0] [0] 0.00/0.56 ? [0 1] x + [1] 0.00/0.56 [0 0] [0] 0.00/0.56 = [c_1(x)] 0.00/0.56 0.00/0.56 [gcd^#(0(), y)] = [0] 0.00/0.56 [0] 0.00/0.56 ? [1] 0.00/0.56 [0] 0.00/0.56 = [c_2(y)] 0.00/0.56 0.00/0.56 [gcd^#(s(x), s(y))] = [4] 0.00/0.56 [0] 0.00/0.56 > [1] 0.00/0.56 [0] 0.00/0.56 = [c_3(x, y, gcd^#(s(x), -(y, x)), gcd^#(-(x, y), s(y)))] 0.00/0.56 0.00/0.56 0.00/0.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.56 0.00/0.56 We are left with following problem, upon which TcT provides the 0.00/0.56 certificate YES(O(1),O(n^1)). 0.00/0.56 0.00/0.56 Strict DPs: 0.00/0.56 { gcd^#(x, 0()) -> c_1(x) 0.00/0.56 , gcd^#(0(), y) -> c_2(y) } 0.00/0.56 Weak DPs: 0.00/0.56 { gcd^#(s(x), s(y)) -> 0.00/0.56 c_3(x, y, gcd^#(s(x), -(y, x)), gcd^#(-(x, y), s(y))) } 0.00/0.56 Obligation: 0.00/0.56 runtime complexity 0.00/0.56 Answer: 0.00/0.56 YES(O(1),O(n^1)) 0.00/0.56 0.00/0.56 We use the processor 'matrix interpretation of dimension 1' to 0.00/0.56 orient following rules strictly. 0.00/0.56 0.00/0.56 DPs: 0.00/0.56 { 1: gcd^#(x, 0()) -> c_1(x) 0.00/0.56 , 2: gcd^#(0(), y) -> c_2(y) } 0.00/0.56 0.00/0.56 Sub-proof: 0.00/0.56 ---------- 0.00/0.56 The following argument positions are usable: 0.00/0.56 none 0.00/0.56 0.00/0.56 TcT has computed the following constructor-based matrix 0.00/0.56 interpretation satisfying not(EDA). 0.00/0.56 0.00/0.56 [0] = [0] 0.00/0.56 0.00/0.56 [s](x1) = [1] x1 + [0] 0.00/0.56 0.00/0.56 [-](x1, x2) = [0] 0.00/0.56 0.00/0.56 [gcd^#](x1, x2) = [4] x1 + [4] x2 + [1] 0.00/0.56 0.00/0.56 [c_1](x1) = [4] x1 + [0] 0.00/0.56 0.00/0.56 [c_2](x1) = [4] x1 + [0] 0.00/0.56 0.00/0.56 [c_3](x1, x2, x3, x4) = [3] x1 + [3] x2 + [1] 0.00/0.56 0.00/0.56 The order satisfies the following ordering constraints: 0.00/0.56 0.00/0.56 [gcd^#(x, 0())] = [4] x + [1] 0.00/0.56 > [4] x + [0] 0.00/0.56 = [c_1(x)] 0.00/0.56 0.00/0.56 [gcd^#(0(), y)] = [4] y + [1] 0.00/0.56 > [4] y + [0] 0.00/0.56 = [c_2(y)] 0.00/0.56 0.00/0.56 [gcd^#(s(x), s(y))] = [4] x + [4] y + [1] 0.00/0.56 >= [3] x + [3] y + [1] 0.00/0.56 = [c_3(x, y, gcd^#(s(x), -(y, x)), gcd^#(-(x, y), s(y)))] 0.00/0.56 0.00/0.56 0.00/0.56 The strictly oriented rules are moved into the weak component. 0.00/0.56 0.00/0.56 We are left with following problem, upon which TcT provides the 0.00/0.56 certificate YES(O(1),O(1)). 0.00/0.56 0.00/0.56 Weak DPs: 0.00/0.56 { gcd^#(x, 0()) -> c_1(x) 0.00/0.56 , gcd^#(0(), y) -> c_2(y) 0.00/0.56 , gcd^#(s(x), s(y)) -> 0.00/0.56 c_3(x, y, gcd^#(s(x), -(y, x)), gcd^#(-(x, y), s(y))) } 0.00/0.56 Obligation: 0.00/0.56 runtime complexity 0.00/0.56 Answer: 0.00/0.56 YES(O(1),O(1)) 0.00/0.56 0.00/0.56 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.56 closed under successors. The DPs are removed. 0.00/0.56 0.00/0.56 { gcd^#(x, 0()) -> c_1(x) 0.00/0.56 , gcd^#(0(), y) -> c_2(y) 0.00/0.56 , gcd^#(s(x), s(y)) -> 0.00/0.56 c_3(x, y, gcd^#(s(x), -(y, x)), gcd^#(-(x, y), s(y))) } 0.00/0.56 0.00/0.56 We are left with following problem, upon which TcT provides the 0.00/0.56 certificate YES(O(1),O(1)). 0.00/0.56 0.00/0.56 Rules: Empty 0.00/0.56 Obligation: 0.00/0.56 runtime complexity 0.00/0.56 Answer: 0.00/0.56 YES(O(1),O(1)) 0.00/0.56 0.00/0.56 Empty rules are trivially bounded 0.00/0.56 0.00/0.56 Hurray, we answered YES(O(1),O(n^1)) 0.00/0.56 EOF