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