YES(O(1),O(n^2)) 159.24/56.66 YES(O(1),O(n^2)) 159.24/56.66 159.24/56.66 We are left with following problem, upon which TcT provides the 159.24/56.66 certificate YES(O(1),O(n^2)). 159.24/56.66 159.24/56.66 Strict Trs: 159.24/56.66 { le(0(), y) -> true() 159.24/56.66 , le(s(x), 0()) -> false() 159.24/56.66 , le(s(x), s(y)) -> le(x, y) 159.24/56.66 , pred(s(x)) -> x 159.24/56.66 , minus(x, 0()) -> x 159.24/56.66 , minus(x, s(y)) -> pred(minus(x, y)) 159.24/56.66 , gcd(0(), y) -> y 159.24/56.66 , gcd(s(x), 0()) -> s(x) 159.24/56.66 , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)) 159.24/56.66 , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y)) 159.24/56.66 , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) } 159.24/56.66 Obligation: 159.24/56.66 innermost runtime complexity 159.24/56.66 Answer: 159.24/56.66 YES(O(1),O(n^2)) 159.24/56.66 159.24/56.66 We add the following dependency tuples: 159.24/56.66 159.24/56.66 Strict DPs: 159.24/56.66 { le^#(0(), y) -> c_1() 159.24/56.66 , le^#(s(x), 0()) -> c_2() 159.24/56.66 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 159.24/56.66 , pred^#(s(x)) -> c_4() 159.24/56.66 , minus^#(x, 0()) -> c_5() 159.24/56.66 , minus^#(x, s(y)) -> c_6(pred^#(minus(x, y)), minus^#(x, y)) 159.24/56.66 , gcd^#(0(), y) -> c_7() 159.24/56.66 , gcd^#(s(x), 0()) -> c_8() 159.24/56.66 , gcd^#(s(x), s(y)) -> 159.24/56.66 c_9(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.66 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.66 c_10(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.66 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.66 c_11(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.66 159.24/56.66 and mark the set of starting terms. 159.24/56.66 159.24/56.66 We are left with following problem, upon which TcT provides the 159.24/56.66 certificate YES(O(1),O(n^2)). 159.24/56.66 159.24/56.66 Strict DPs: 159.24/56.66 { le^#(0(), y) -> c_1() 159.24/56.66 , le^#(s(x), 0()) -> c_2() 159.24/56.66 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 159.24/56.66 , pred^#(s(x)) -> c_4() 159.24/56.66 , minus^#(x, 0()) -> c_5() 159.24/56.66 , minus^#(x, s(y)) -> c_6(pred^#(minus(x, y)), minus^#(x, y)) 159.24/56.66 , gcd^#(0(), y) -> c_7() 159.24/56.66 , gcd^#(s(x), 0()) -> c_8() 159.24/56.66 , gcd^#(s(x), s(y)) -> 159.24/56.66 c_9(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.66 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.66 c_10(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.66 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.66 c_11(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.66 Weak Trs: 159.24/56.66 { le(0(), y) -> true() 159.24/56.66 , le(s(x), 0()) -> false() 159.24/56.66 , le(s(x), s(y)) -> le(x, y) 159.24/56.66 , pred(s(x)) -> x 159.24/56.66 , minus(x, 0()) -> x 159.24/56.66 , minus(x, s(y)) -> pred(minus(x, y)) 159.24/56.66 , gcd(0(), y) -> y 159.24/56.66 , gcd(s(x), 0()) -> s(x) 159.24/56.66 , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)) 159.24/56.66 , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y)) 159.24/56.66 , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) } 159.24/56.66 Obligation: 159.24/56.66 innermost runtime complexity 159.24/56.66 Answer: 159.24/56.66 YES(O(1),O(n^2)) 159.24/56.66 159.24/56.66 We estimate the number of application of {1,2,4,5,7,8} by 159.24/56.66 applications of Pre({1,2,4,5,7,8}) = {3,6,9,10,11}. Here rules are 159.24/56.66 labeled as follows: 159.24/56.66 159.24/56.66 DPs: 159.24/56.66 { 1: le^#(0(), y) -> c_1() 159.24/56.66 , 2: le^#(s(x), 0()) -> c_2() 159.24/56.66 , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y)) 159.24/56.66 , 4: pred^#(s(x)) -> c_4() 159.24/56.66 , 5: minus^#(x, 0()) -> c_5() 159.24/56.66 , 6: minus^#(x, s(y)) -> c_6(pred^#(minus(x, y)), minus^#(x, y)) 159.24/56.66 , 7: gcd^#(0(), y) -> c_7() 159.24/56.66 , 8: gcd^#(s(x), 0()) -> c_8() 159.24/56.66 , 9: gcd^#(s(x), s(y)) -> 159.24/56.66 c_9(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.66 , 10: if_gcd^#(true(), s(x), s(y)) -> 159.24/56.66 c_10(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.66 , 11: if_gcd^#(false(), s(x), s(y)) -> 159.24/56.66 c_11(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.66 159.24/56.66 We are left with following problem, upon which TcT provides the 159.24/56.66 certificate YES(O(1),O(n^2)). 159.24/56.66 159.24/56.66 Strict DPs: 159.24/56.66 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 159.24/56.66 , minus^#(x, s(y)) -> c_6(pred^#(minus(x, y)), minus^#(x, y)) 159.24/56.66 , gcd^#(s(x), s(y)) -> 159.24/56.66 c_9(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.66 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.66 c_10(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.66 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.66 c_11(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.66 Weak DPs: 159.24/56.66 { le^#(0(), y) -> c_1() 159.24/56.66 , le^#(s(x), 0()) -> c_2() 159.24/56.66 , pred^#(s(x)) -> c_4() 159.24/56.66 , minus^#(x, 0()) -> c_5() 159.24/56.66 , gcd^#(0(), y) -> c_7() 159.24/56.66 , gcd^#(s(x), 0()) -> c_8() } 159.24/56.66 Weak Trs: 159.24/56.66 { le(0(), y) -> true() 159.24/56.66 , le(s(x), 0()) -> false() 159.24/56.66 , le(s(x), s(y)) -> le(x, y) 159.24/56.66 , pred(s(x)) -> x 159.24/56.66 , minus(x, 0()) -> x 159.24/56.66 , minus(x, s(y)) -> pred(minus(x, y)) 159.24/56.66 , gcd(0(), y) -> y 159.24/56.66 , gcd(s(x), 0()) -> s(x) 159.24/56.66 , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)) 159.24/56.66 , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y)) 159.24/56.66 , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) } 159.24/56.66 Obligation: 159.24/56.66 innermost runtime complexity 159.24/56.66 Answer: 159.24/56.66 YES(O(1),O(n^2)) 159.24/56.66 159.24/56.66 The following weak DPs constitute a sub-graph of the DG that is 159.24/56.66 closed under successors. The DPs are removed. 159.24/56.66 159.24/56.66 { le^#(0(), y) -> c_1() 159.24/56.66 , le^#(s(x), 0()) -> c_2() 159.24/56.66 , pred^#(s(x)) -> c_4() 159.24/56.66 , minus^#(x, 0()) -> c_5() 159.24/56.66 , gcd^#(0(), y) -> c_7() 159.24/56.66 , gcd^#(s(x), 0()) -> c_8() } 159.24/56.66 159.24/56.66 We are left with following problem, upon which TcT provides the 159.24/56.66 certificate YES(O(1),O(n^2)). 159.24/56.66 159.24/56.66 Strict DPs: 159.24/56.66 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 159.24/56.66 , minus^#(x, s(y)) -> c_6(pred^#(minus(x, y)), minus^#(x, y)) 159.24/56.66 , gcd^#(s(x), s(y)) -> 159.24/56.66 c_9(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.66 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.66 c_10(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.66 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.66 c_11(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.66 Weak Trs: 159.24/56.66 { le(0(), y) -> true() 159.24/56.66 , le(s(x), 0()) -> false() 159.24/56.66 , le(s(x), s(y)) -> le(x, y) 159.24/56.66 , pred(s(x)) -> x 159.24/56.66 , minus(x, 0()) -> x 159.24/56.66 , minus(x, s(y)) -> pred(minus(x, y)) 159.24/56.66 , gcd(0(), y) -> y 159.24/56.66 , gcd(s(x), 0()) -> s(x) 159.24/56.66 , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)) 159.24/56.66 , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y)) 159.24/56.66 , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) } 159.24/56.66 Obligation: 159.24/56.66 innermost runtime complexity 159.24/56.66 Answer: 159.24/56.66 YES(O(1),O(n^2)) 159.24/56.66 159.24/56.66 Due to missing edges in the dependency-graph, the right-hand sides 159.24/56.66 of following rules could be simplified: 159.24/56.66 159.24/56.66 { minus^#(x, s(y)) -> c_6(pred^#(minus(x, y)), minus^#(x, y)) } 159.24/56.66 159.24/56.66 We are left with following problem, upon which TcT provides the 159.24/56.66 certificate YES(O(1),O(n^2)). 159.24/56.66 159.24/56.66 Strict DPs: 159.24/56.66 { le^#(s(x), s(y)) -> c_1(le^#(x, y)) 159.24/56.66 , minus^#(x, s(y)) -> c_2(minus^#(x, y)) 159.24/56.66 , gcd^#(s(x), s(y)) -> 159.24/56.66 c_3(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.66 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.66 c_4(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.66 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.66 c_5(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.66 Weak Trs: 159.24/56.66 { le(0(), y) -> true() 159.24/56.66 , le(s(x), 0()) -> false() 159.24/56.66 , le(s(x), s(y)) -> le(x, y) 159.24/56.66 , pred(s(x)) -> x 159.24/56.66 , minus(x, 0()) -> x 159.24/56.66 , minus(x, s(y)) -> pred(minus(x, y)) 159.24/56.66 , gcd(0(), y) -> y 159.24/56.66 , gcd(s(x), 0()) -> s(x) 159.24/56.66 , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)) 159.24/56.66 , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y)) 159.24/56.66 , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) } 159.24/56.66 Obligation: 159.24/56.66 innermost runtime complexity 159.24/56.66 Answer: 159.24/56.66 YES(O(1),O(n^2)) 159.24/56.66 159.24/56.66 We replace rewrite rules by usable rules: 159.24/56.66 159.24/56.66 Weak Usable Rules: 159.24/56.66 { le(0(), y) -> true() 159.24/56.66 , le(s(x), 0()) -> false() 159.24/56.66 , le(s(x), s(y)) -> le(x, y) 159.24/56.66 , pred(s(x)) -> x 159.24/56.66 , minus(x, 0()) -> x 159.24/56.66 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.66 159.24/56.66 We are left with following problem, upon which TcT provides the 159.24/56.66 certificate YES(O(1),O(n^2)). 159.24/56.66 159.24/56.66 Strict DPs: 159.24/56.66 { le^#(s(x), s(y)) -> c_1(le^#(x, y)) 159.24/56.66 , minus^#(x, s(y)) -> c_2(minus^#(x, y)) 159.24/56.66 , gcd^#(s(x), s(y)) -> 159.24/56.66 c_3(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.66 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.66 c_4(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.66 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.66 c_5(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.66 Weak Trs: 159.24/56.66 { le(0(), y) -> true() 159.24/56.66 , le(s(x), 0()) -> false() 159.24/56.66 , le(s(x), s(y)) -> le(x, y) 159.24/56.66 , pred(s(x)) -> x 159.24/56.66 , minus(x, 0()) -> x 159.24/56.66 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.66 Obligation: 159.24/56.66 innermost runtime complexity 159.24/56.66 Answer: 159.24/56.66 YES(O(1),O(n^2)) 159.24/56.66 159.24/56.66 We use the processor 'matrix interpretation of dimension 2' to 159.24/56.66 orient following rules strictly. 159.24/56.66 159.24/56.66 DPs: 159.24/56.66 { 1: le^#(s(x), s(y)) -> c_1(le^#(x, y)) } 159.24/56.66 Trs: 159.24/56.66 { le(0(), y) -> true() 159.24/56.66 , le(s(x), 0()) -> false() 159.24/56.66 , pred(s(x)) -> x } 159.24/56.66 159.24/56.66 Sub-proof: 159.24/56.66 ---------- 159.24/56.66 The following argument positions are usable: 159.24/56.66 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, 159.24/56.66 Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2} 159.24/56.66 159.24/56.66 TcT has computed the following constructor-based matrix 159.24/56.66 interpretation satisfying not(EDA). 159.24/56.66 159.24/56.66 [le](x1, x2) = [0 0] x2 + [4] 159.24/56.66 [1 3] [0] 159.24/56.66 159.24/56.66 [0] = [0] 159.24/56.66 [0] 159.24/56.66 159.24/56.66 [true] = [0] 159.24/56.66 [0] 159.24/56.66 159.24/56.66 [s](x1) = [1 0] x1 + [1] 159.24/56.66 [1 1] [0] 159.24/56.66 159.24/56.66 [false] = [1] 159.24/56.66 [0] 159.24/56.66 159.24/56.66 [pred](x1) = [1 0] x1 + [0] 159.24/56.66 [0 1] [0] 159.24/56.66 159.24/56.66 [minus](x1, x2) = [1 0] x1 + [0] 159.24/56.66 [0 1] [0] 159.24/56.66 159.24/56.66 [le^#](x1, x2) = [0 0] x1 + [1 0] x2 + [0] 159.24/56.66 [0 4] [4 4] [0] 159.24/56.66 159.24/56.66 [minus^#](x1, x2) = [0 0] x1 + [0] 159.24/56.66 [4 0] [0] 159.24/56.66 159.24/56.66 [gcd^#](x1, x2) = [2 2] x1 + [0 2] x2 + [0] 159.24/56.66 [0 0] [0 0] [4] 159.24/56.66 159.24/56.66 [if_gcd^#](x1, x2, x3) = [0 0] x1 + [0 2] x2 + [0 2] x3 + [0] 159.24/56.66 [4 0] [0 0] [0 0] [0] 159.24/56.66 159.24/56.66 [c_1](x1) = [1 0] x1 + [0] 159.24/56.66 [0 0] [3] 159.24/56.66 159.24/56.66 [c_2](x1) = [2 0] x1 + [0] 159.24/56.66 [0 0] [0] 159.24/56.66 159.24/56.66 [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 159.24/56.66 [0 0] [0 0] [3] 159.24/56.66 159.24/56.66 [c_4](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 159.24/56.66 [0 0] [0 0] [0] 159.24/56.66 159.24/56.66 [c_5](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 159.24/56.66 [0 0] [0 0] [3] 159.24/56.66 159.24/56.66 The order satisfies the following ordering constraints: 159.24/56.66 159.24/56.66 [le(0(), y)] = [0 0] y + [4] 159.24/56.66 [1 3] [0] 159.24/56.66 > [0] 159.24/56.66 [0] 159.24/56.66 = [true()] 159.24/56.66 159.24/56.66 [le(s(x), 0())] = [4] 159.24/56.66 [0] 159.24/56.66 > [1] 159.24/56.66 [0] 159.24/56.66 = [false()] 159.24/56.66 159.24/56.66 [le(s(x), s(y))] = [0 0] y + [4] 159.24/56.66 [4 3] [1] 159.24/56.66 >= [0 0] y + [4] 159.24/56.66 [1 3] [0] 159.24/56.66 = [le(x, y)] 159.24/56.66 159.24/56.66 [pred(s(x))] = [1 0] x + [1] 159.24/56.66 [1 1] [0] 159.24/56.66 > [1 0] x + [0] 159.24/56.66 [0 1] [0] 159.24/56.66 = [x] 159.24/56.66 159.24/56.66 [minus(x, 0())] = [1 0] x + [0] 159.24/56.66 [0 1] [0] 159.24/56.66 >= [1 0] x + [0] 159.24/56.66 [0 1] [0] 159.24/56.66 = [x] 159.24/56.66 159.24/56.66 [minus(x, s(y))] = [1 0] x + [0] 159.24/56.66 [0 1] [0] 159.24/56.66 >= [1 0] x + [0] 159.24/56.66 [0 1] [0] 159.24/56.66 = [pred(minus(x, y))] 159.24/56.66 159.24/56.66 [le^#(s(x), s(y))] = [1 0] y + [0 0] x + [1] 159.24/56.66 [8 4] [4 4] [4] 159.24/56.66 > [1 0] y + [0] 159.24/56.66 [0 0] [3] 159.24/56.66 = [c_1(le^#(x, y))] 159.24/56.66 159.24/56.66 [minus^#(x, s(y))] = [0 0] x + [0] 159.24/56.66 [4 0] [0] 159.24/56.66 >= [0] 159.24/56.66 [0] 159.24/56.66 = [c_2(minus^#(x, y))] 159.24/56.66 159.24/56.66 [gcd^#(s(x), s(y))] = [2 2] y + [4 2] x + [2] 159.24/56.66 [0 0] [0 0] [4] 159.24/56.66 >= [2 2] y + [3 2] x + [2] 159.24/56.66 [0 0] [0 0] [3] 159.24/56.66 = [c_3(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x))] 159.24/56.66 159.24/56.66 [if_gcd^#(true(), s(x), s(y))] = [2 2] y + [2 2] x + [0] 159.24/56.66 [0 0] [0 0] [0] 159.24/56.66 >= [2 2] y + [2 2] x + [0] 159.24/56.66 [0 0] [0 0] [0] 159.24/56.67 = [c_4(gcd^#(minus(x, y), s(y)), minus^#(x, y))] 159.24/56.67 159.24/56.67 [if_gcd^#(false(), s(x), s(y))] = [2 2] y + [2 2] x + [0] 159.24/56.67 [0 0] [0 0] [4] 159.24/56.67 >= [2 2] y + [2 2] x + [0] 159.24/56.67 [0 0] [0 0] [3] 159.24/56.67 = [c_5(gcd^#(minus(y, x), s(x)), minus^#(y, x))] 159.24/56.67 159.24/56.67 159.24/56.67 The strictly oriented rules are moved into the weak component. 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(n^2)). 159.24/56.67 159.24/56.67 Strict DPs: 159.24/56.67 { minus^#(x, s(y)) -> c_2(minus^#(x, y)) 159.24/56.67 , gcd^#(s(x), s(y)) -> 159.24/56.67 c_3(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_5(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 Weak DPs: { le^#(s(x), s(y)) -> c_1(le^#(x, y)) } 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(n^2)) 159.24/56.67 159.24/56.67 The following weak DPs constitute a sub-graph of the DG that is 159.24/56.67 closed under successors. The DPs are removed. 159.24/56.67 159.24/56.67 { le^#(s(x), s(y)) -> c_1(le^#(x, y)) } 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(n^2)). 159.24/56.67 159.24/56.67 Strict DPs: 159.24/56.67 { minus^#(x, s(y)) -> c_2(minus^#(x, y)) 159.24/56.67 , gcd^#(s(x), s(y)) -> 159.24/56.67 c_3(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_5(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(n^2)) 159.24/56.67 159.24/56.67 Due to missing edges in the dependency-graph, the right-hand sides 159.24/56.67 of following rules could be simplified: 159.24/56.67 159.24/56.67 { gcd^#(s(x), s(y)) -> 159.24/56.67 c_3(if_gcd^#(le(y, x), s(x), s(y)), le^#(y, x)) } 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(n^2)). 159.24/56.67 159.24/56.67 Strict DPs: 159.24/56.67 { minus^#(x, s(y)) -> c_1(minus^#(x, y)) 159.24/56.67 , gcd^#(s(x), s(y)) -> c_2(if_gcd^#(le(y, x), s(x), s(y))) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_3(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(n^2)) 159.24/56.67 159.24/56.67 We decompose the input problem according to the dependency graph 159.24/56.67 into the upper component 159.24/56.67 159.24/56.67 { gcd^#(s(x), s(y)) -> c_2(if_gcd^#(le(y, x), s(x), s(y))) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_3(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 159.24/56.67 and lower component 159.24/56.67 159.24/56.67 { minus^#(x, s(y)) -> c_1(minus^#(x, y)) } 159.24/56.67 159.24/56.67 Further, following extension rules are added to the lower 159.24/56.67 component. 159.24/56.67 159.24/56.67 { gcd^#(s(x), s(y)) -> if_gcd^#(le(y, x), s(x), s(y)) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> minus^#(x, y) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> gcd^#(minus(x, y), s(y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> minus^#(y, x) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> gcd^#(minus(y, x), s(x)) } 159.24/56.67 159.24/56.67 TcT solves the upper component with certificate YES(O(1),O(n^1)). 159.24/56.67 159.24/56.67 Sub-proof: 159.24/56.67 ---------- 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(n^1)). 159.24/56.67 159.24/56.67 Strict DPs: 159.24/56.67 { gcd^#(s(x), s(y)) -> c_2(if_gcd^#(le(y, x), s(x), s(y))) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_3(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(n^1)) 159.24/56.67 159.24/56.67 We use the processor 'matrix interpretation of dimension 1' to 159.24/56.67 orient following rules strictly. 159.24/56.67 159.24/56.67 DPs: 159.24/56.67 { 2: if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_3(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , 3: if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 Trs: { pred(s(x)) -> x } 159.24/56.67 159.24/56.67 Sub-proof: 159.24/56.67 ---------- 159.24/56.67 The following argument positions are usable: 159.24/56.67 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1} 159.24/56.67 159.24/56.67 TcT has computed the following constructor-based matrix 159.24/56.67 interpretation satisfying not(EDA). 159.24/56.67 159.24/56.67 [le](x1, x2) = [0] 159.24/56.67 159.24/56.67 [0] = [0] 159.24/56.67 159.24/56.67 [true] = [0] 159.24/56.67 159.24/56.67 [s](x1) = [1] x1 + [4] 159.24/56.67 159.24/56.67 [false] = [0] 159.24/56.67 159.24/56.67 [pred](x1) = [1] x1 + [0] 159.24/56.67 159.24/56.67 [minus](x1, x2) = [1] x1 + [0] 159.24/56.67 159.24/56.67 [minus^#](x1, x2) = [0] 159.24/56.67 159.24/56.67 [gcd^#](x1, x2) = [1] x1 + [1] x2 + [0] 159.24/56.67 159.24/56.67 [if_gcd^#](x1, x2, x3) = [1] x2 + [1] x3 + [0] 159.24/56.67 159.24/56.67 [c_2](x1) = [1] x1 + [0] 159.24/56.67 159.24/56.67 [c_3](x1, x2) = [1] x1 + [1] 159.24/56.67 159.24/56.67 [c_4](x1, x2) = [1] x1 + [3] 159.24/56.67 159.24/56.67 The order satisfies the following ordering constraints: 159.24/56.67 159.24/56.67 [le(0(), y)] = [0] 159.24/56.67 >= [0] 159.24/56.67 = [true()] 159.24/56.67 159.24/56.67 [le(s(x), 0())] = [0] 159.24/56.67 >= [0] 159.24/56.67 = [false()] 159.24/56.67 159.24/56.67 [le(s(x), s(y))] = [0] 159.24/56.67 >= [0] 159.24/56.67 = [le(x, y)] 159.24/56.67 159.24/56.67 [pred(s(x))] = [1] x + [4] 159.24/56.67 > [1] x + [0] 159.24/56.67 = [x] 159.24/56.67 159.24/56.67 [minus(x, 0())] = [1] x + [0] 159.24/56.67 >= [1] x + [0] 159.24/56.67 = [x] 159.24/56.67 159.24/56.67 [minus(x, s(y))] = [1] x + [0] 159.24/56.67 >= [1] x + [0] 159.24/56.67 = [pred(minus(x, y))] 159.24/56.67 159.24/56.67 [gcd^#(s(x), s(y))] = [1] y + [1] x + [8] 159.24/56.67 >= [1] y + [1] x + [8] 159.24/56.67 = [c_2(if_gcd^#(le(y, x), s(x), s(y)))] 159.24/56.67 159.24/56.67 [if_gcd^#(true(), s(x), s(y))] = [1] y + [1] x + [8] 159.24/56.67 > [1] y + [1] x + [5] 159.24/56.67 = [c_3(gcd^#(minus(x, y), s(y)), minus^#(x, y))] 159.24/56.67 159.24/56.67 [if_gcd^#(false(), s(x), s(y))] = [1] y + [1] x + [8] 159.24/56.67 > [1] y + [1] x + [7] 159.24/56.67 = [c_4(gcd^#(minus(y, x), s(x)), minus^#(y, x))] 159.24/56.67 159.24/56.67 159.24/56.67 We return to the main proof. Consider the set of all dependency 159.24/56.67 pairs 159.24/56.67 159.24/56.67 : 159.24/56.67 { 1: gcd^#(s(x), s(y)) -> c_2(if_gcd^#(le(y, x), s(x), s(y))) 159.24/56.67 , 2: if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_3(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , 3: if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 159.24/56.67 Processor 'matrix interpretation of dimension 1' induces the 159.24/56.67 complexity certificate YES(?,O(n^1)) on application of dependency 159.24/56.67 pairs {2,3}. These cover all (indirect) predecessors of dependency 159.24/56.67 pairs {1,2,3}, their number of application is equally bounded. The 159.24/56.67 dependency pairs are shifted into the weak component. 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(1)). 159.24/56.67 159.24/56.67 Weak DPs: 159.24/56.67 { gcd^#(s(x), s(y)) -> c_2(if_gcd^#(le(y, x), s(x), s(y))) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_3(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(1)) 159.24/56.67 159.24/56.67 The following weak DPs constitute a sub-graph of the DG that is 159.24/56.67 closed under successors. The DPs are removed. 159.24/56.67 159.24/56.67 { gcd^#(s(x), s(y)) -> c_2(if_gcd^#(le(y, x), s(x), s(y))) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> 159.24/56.67 c_3(gcd^#(minus(x, y), s(y)), minus^#(x, y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> 159.24/56.67 c_4(gcd^#(minus(y, x), s(x)), minus^#(y, x)) } 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(1)). 159.24/56.67 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(1)) 159.24/56.67 159.24/56.67 No rule is usable, rules are removed from the input problem. 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(1)). 159.24/56.67 159.24/56.67 Rules: Empty 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(1)) 159.24/56.67 159.24/56.67 Empty rules are trivially bounded 159.24/56.67 159.24/56.67 We return to the main proof. 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(n^1)). 159.24/56.67 159.24/56.67 Strict DPs: { minus^#(x, s(y)) -> c_1(minus^#(x, y)) } 159.24/56.67 Weak DPs: 159.24/56.67 { gcd^#(s(x), s(y)) -> if_gcd^#(le(y, x), s(x), s(y)) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> minus^#(x, y) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> gcd^#(minus(x, y), s(y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> minus^#(y, x) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> gcd^#(minus(y, x), s(x)) } 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(n^1)) 159.24/56.67 159.24/56.67 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 159.24/56.67 to orient following rules strictly. 159.24/56.67 159.24/56.67 DPs: 159.24/56.67 { 1: minus^#(x, s(y)) -> c_1(minus^#(x, y)) 159.24/56.67 , 3: if_gcd^#(true(), s(x), s(y)) -> minus^#(x, y) 159.24/56.67 , 4: if_gcd^#(true(), s(x), s(y)) -> gcd^#(minus(x, y), s(y)) 159.24/56.67 , 5: if_gcd^#(false(), s(x), s(y)) -> minus^#(y, x) 159.24/56.67 , 6: if_gcd^#(false(), s(x), s(y)) -> gcd^#(minus(y, x), s(x)) } 159.24/56.67 Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , pred(s(x)) -> x } 159.24/56.67 159.24/56.67 Sub-proof: 159.24/56.67 ---------- 159.24/56.67 The input was oriented with the instance of 'Small Polynomial Path 159.24/56.67 Order (PS,1-bounded)' as induced by the safe mapping 159.24/56.67 159.24/56.67 safe(le) = {1}, safe(0) = {}, safe(true) = {}, safe(s) = {1}, 159.24/56.67 safe(false) = {}, safe(pred) = {}, safe(minus) = {}, 159.24/56.67 safe(minus^#) = {}, safe(gcd^#) = {}, safe(if_gcd^#) = {1}, 159.24/56.67 safe(c_1) = {} 159.24/56.67 159.24/56.67 and precedence 159.24/56.67 159.24/56.67 le ~ minus^#, le ~ if_gcd^#, pred ~ minus, minus^# ~ gcd^#, 159.24/56.67 minus^# ~ if_gcd^#, gcd^# ~ if_gcd^# . 159.24/56.67 159.24/56.67 Following symbols are considered recursive: 159.24/56.67 159.24/56.67 {minus^#, gcd^#, if_gcd^#} 159.24/56.67 159.24/56.67 The recursion depth is 1. 159.24/56.67 159.24/56.67 Further, following argument filtering is employed: 159.24/56.67 159.24/56.67 pi(le) = [1, 2], pi(0) = [], pi(true) = [], pi(s) = [1], 159.24/56.67 pi(false) = [], pi(pred) = 1, pi(minus) = 1, pi(minus^#) = [1, 2], 159.24/56.67 pi(gcd^#) = [1, 2], pi(if_gcd^#) = [2, 3], pi(c_1) = [1] 159.24/56.67 159.24/56.67 Usable defined function symbols are a subset of: 159.24/56.67 159.24/56.67 {pred, minus, minus^#, gcd^#, if_gcd^#} 159.24/56.67 159.24/56.67 For your convenience, here are the satisfied ordering constraints: 159.24/56.67 159.24/56.67 pi(minus^#(x, s(y))) = minus^#(x, s(; y);) 159.24/56.67 > c_1(minus^#(x, y;);) 159.24/56.67 = pi(c_1(minus^#(x, y))) 159.24/56.67 159.24/56.67 pi(gcd^#(s(x), s(y))) = gcd^#(s(; x), s(; y);) 159.24/56.67 >= if_gcd^#(s(; x), s(; y);) 159.24/56.67 = pi(if_gcd^#(le(y, x), s(x), s(y))) 159.24/56.67 159.24/56.67 pi(if_gcd^#(true(), s(x), s(y))) = if_gcd^#(s(; x), s(; y);) 159.24/56.67 > minus^#(x, y;) 159.24/56.67 = pi(minus^#(x, y)) 159.24/56.67 159.24/56.67 pi(if_gcd^#(true(), s(x), s(y))) = if_gcd^#(s(; x), s(; y);) 159.24/56.67 > gcd^#(x, s(; y);) 159.24/56.67 = pi(gcd^#(minus(x, y), s(y))) 159.24/56.67 159.24/56.67 pi(if_gcd^#(false(), s(x), s(y))) = if_gcd^#(s(; x), s(; y);) 159.24/56.67 > minus^#(y, x;) 159.24/56.67 = pi(minus^#(y, x)) 159.24/56.67 159.24/56.67 pi(if_gcd^#(false(), s(x), s(y))) = if_gcd^#(s(; x), s(; y);) 159.24/56.67 > gcd^#(y, s(; x);) 159.24/56.67 = pi(gcd^#(minus(y, x), s(x))) 159.24/56.67 159.24/56.67 pi(pred(s(x))) = s(; x) 159.24/56.67 > x 159.24/56.67 = pi(x) 159.24/56.67 159.24/56.67 pi(minus(x, 0())) = x 159.24/56.67 >= x 159.24/56.67 = pi(x) 159.24/56.67 159.24/56.67 pi(minus(x, s(y))) = x 159.24/56.67 >= x 159.24/56.67 = pi(pred(minus(x, y))) 159.24/56.67 159.24/56.67 159.24/56.67 We return to the main proof. Consider the set of all dependency 159.24/56.67 pairs 159.24/56.67 159.24/56.67 : 159.24/56.67 { 1: minus^#(x, s(y)) -> c_1(minus^#(x, y)) 159.24/56.67 , 2: gcd^#(s(x), s(y)) -> if_gcd^#(le(y, x), s(x), s(y)) 159.24/56.67 , 3: if_gcd^#(true(), s(x), s(y)) -> minus^#(x, y) 159.24/56.67 , 4: if_gcd^#(true(), s(x), s(y)) -> gcd^#(minus(x, y), s(y)) 159.24/56.67 , 5: if_gcd^#(false(), s(x), s(y)) -> minus^#(y, x) 159.24/56.67 , 6: if_gcd^#(false(), s(x), s(y)) -> gcd^#(minus(y, x), s(x)) } 159.24/56.67 159.24/56.67 Processor 'Small Polynomial Path Order (PS,1-bounded)' induces the 159.24/56.67 complexity certificate YES(?,O(n^1)) on application of dependency 159.24/56.67 pairs {1,3,4,5,6}. These cover all (indirect) predecessors of 159.24/56.67 dependency pairs {1,2,3,4,5,6}, their number of application is 159.24/56.67 equally bounded. The dependency pairs are shifted into the weak 159.24/56.67 component. 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(1)). 159.24/56.67 159.24/56.67 Weak DPs: 159.24/56.67 { minus^#(x, s(y)) -> c_1(minus^#(x, y)) 159.24/56.67 , gcd^#(s(x), s(y)) -> if_gcd^#(le(y, x), s(x), s(y)) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> minus^#(x, y) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> gcd^#(minus(x, y), s(y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> minus^#(y, x) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> gcd^#(minus(y, x), s(x)) } 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(1)) 159.24/56.67 159.24/56.67 The following weak DPs constitute a sub-graph of the DG that is 159.24/56.67 closed under successors. The DPs are removed. 159.24/56.67 159.24/56.67 { minus^#(x, s(y)) -> c_1(minus^#(x, y)) 159.24/56.67 , gcd^#(s(x), s(y)) -> if_gcd^#(le(y, x), s(x), s(y)) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> minus^#(x, y) 159.24/56.67 , if_gcd^#(true(), s(x), s(y)) -> gcd^#(minus(x, y), s(y)) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> minus^#(y, x) 159.24/56.67 , if_gcd^#(false(), s(x), s(y)) -> gcd^#(minus(y, x), s(x)) } 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(1)). 159.24/56.67 159.24/56.67 Weak Trs: 159.24/56.67 { le(0(), y) -> true() 159.24/56.67 , le(s(x), 0()) -> false() 159.24/56.67 , le(s(x), s(y)) -> le(x, y) 159.24/56.67 , pred(s(x)) -> x 159.24/56.67 , minus(x, 0()) -> x 159.24/56.67 , minus(x, s(y)) -> pred(minus(x, y)) } 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(1)) 159.24/56.67 159.24/56.67 No rule is usable, rules are removed from the input problem. 159.24/56.67 159.24/56.67 We are left with following problem, upon which TcT provides the 159.24/56.67 certificate YES(O(1),O(1)). 159.24/56.67 159.24/56.67 Rules: Empty 159.24/56.67 Obligation: 159.24/56.67 innermost runtime complexity 159.24/56.67 Answer: 159.24/56.67 YES(O(1),O(1)) 159.24/56.67 159.24/56.67 Empty rules are trivially bounded 159.24/56.67 159.24/56.67 Hurray, we answered YES(O(1),O(n^2)) 159.39/56.75 EOF