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