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