YES(O(1),O(n^2)) 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , quot(0(), s(y)) -> 0() 476.09/148.03 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 We add the following dependency tuples: 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(x, 0()) -> c_1() 476.09/148.03 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 476.09/148.03 , quot^#(0(), s(y)) -> c_3() 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 476.09/148.03 , plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(minus(y, s(s(z))), minus(x, s(0()))), 476.09/148.03 minus^#(y, s(s(z))), 476.09/148.03 minus^#(x, s(0()))) 476.09/148.03 , plus^#(0(), y) -> c_6() 476.09/148.03 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_8(plus^#(plus(y, s(s(z))), plus(x, s(0()))), 476.09/148.03 plus^#(y, s(s(z))), 476.09/148.03 plus^#(x, s(0()))) } 476.09/148.03 476.09/148.03 and mark the set of starting terms. 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(x, 0()) -> c_1() 476.09/148.03 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 476.09/148.03 , quot^#(0(), s(y)) -> c_3() 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 476.09/148.03 , plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(minus(y, s(s(z))), minus(x, s(0()))), 476.09/148.03 minus^#(y, s(s(z))), 476.09/148.03 minus^#(x, s(0()))) 476.09/148.03 , plus^#(0(), y) -> c_6() 476.09/148.03 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_8(plus^#(plus(y, s(s(z))), plus(x, s(0()))), 476.09/148.03 plus^#(y, s(s(z))), 476.09/148.03 plus^#(x, s(0()))) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , quot(0(), s(y)) -> 0() 476.09/148.03 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 We estimate the number of application of {1,3,6} by applications of 476.09/148.03 Pre({1,3,6}) = {2,4,5,7,8}. Here rules are labeled as follows: 476.09/148.03 476.09/148.03 DPs: 476.09/148.03 { 1: minus^#(x, 0()) -> c_1() 476.09/148.03 , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 476.09/148.03 , 3: quot^#(0(), s(y)) -> c_3() 476.09/148.03 , 4: quot^#(s(x), s(y)) -> 476.09/148.03 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 476.09/148.03 , 5: plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(minus(y, s(s(z))), minus(x, s(0()))), 476.09/148.03 minus^#(y, s(s(z))), 476.09/148.03 minus^#(x, s(0()))) 476.09/148.03 , 6: plus^#(0(), y) -> c_6() 476.09/148.03 , 7: plus^#(s(x), y) -> c_7(plus^#(x, y)) 476.09/148.03 , 8: plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_8(plus^#(plus(y, s(s(z))), plus(x, s(0()))), 476.09/148.03 plus^#(y, s(s(z))), 476.09/148.03 plus^#(x, s(0()))) } 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 476.09/148.03 , plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(minus(y, s(s(z))), minus(x, s(0()))), 476.09/148.03 minus^#(y, s(s(z))), 476.09/148.03 minus^#(x, s(0()))) 476.09/148.03 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_8(plus^#(plus(y, s(s(z))), plus(x, s(0()))), 476.09/148.03 plus^#(y, s(s(z))), 476.09/148.03 plus^#(x, s(0()))) } 476.09/148.03 Weak DPs: 476.09/148.03 { minus^#(x, 0()) -> c_1() 476.09/148.03 , quot^#(0(), s(y)) -> c_3() 476.09/148.03 , plus^#(0(), y) -> c_6() } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , quot(0(), s(y)) -> 0() 476.09/148.03 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 The following weak DPs constitute a sub-graph of the DG that is 476.09/148.03 closed under successors. The DPs are removed. 476.09/148.03 476.09/148.03 { minus^#(x, 0()) -> c_1() 476.09/148.03 , quot^#(0(), s(y)) -> c_3() 476.09/148.03 , plus^#(0(), y) -> c_6() } 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 476.09/148.03 , plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(minus(y, s(s(z))), minus(x, s(0()))), 476.09/148.03 minus^#(y, s(s(z))), 476.09/148.03 minus^#(x, s(0()))) 476.09/148.03 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_8(plus^#(plus(y, s(s(z))), plus(x, s(0()))), 476.09/148.03 plus^#(y, s(s(z))), 476.09/148.03 plus^#(x, s(0()))) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , quot(0(), s(y)) -> 0() 476.09/148.03 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 Due to missing edges in the dependency-graph, the right-hand sides 476.09/148.03 of following rules could be simplified: 476.09/148.03 476.09/148.03 { plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(minus(y, s(s(z))), minus(x, s(0()))), 476.09/148.03 minus^#(y, s(s(z))), 476.09/148.03 minus^#(x, s(0()))) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_8(plus^#(plus(y, s(s(z))), plus(x, s(0()))), 476.09/148.03 plus^#(y, s(s(z))), 476.09/148.03 plus^#(x, s(0()))) } 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 476.09/148.03 , plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_3(plus^#(minus(y, s(s(z))), minus(x, s(0())))) 476.09/148.03 , plus^#(s(x), y) -> c_4(plus^#(x, y)) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(plus(y, s(s(z))), plus(x, s(0())))) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , quot(0(), s(y)) -> 0() 476.09/148.03 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 We replace rewrite rules by usable rules: 476.09/148.03 476.09/148.03 Weak Usable Rules: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 476.09/148.03 , plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_3(plus^#(minus(y, s(s(z))), minus(x, s(0())))) 476.09/148.03 , plus^#(s(x), y) -> c_4(plus^#(x, y)) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(plus(y, s(s(z))), plus(x, s(0())))) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 We use the processor 'matrix interpretation of dimension 1' to 476.09/148.03 orient following rules strictly. 476.09/148.03 476.09/148.03 DPs: 476.09/148.03 { 3: plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_3(plus^#(minus(y, s(s(z))), minus(x, s(0())))) 476.09/148.03 , 5: plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(plus(y, s(s(z))), plus(x, s(0())))) } 476.09/148.03 Trs: { plus(s(x), y) -> s(plus(x, y)) } 476.09/148.03 476.09/148.03 Sub-proof: 476.09/148.03 ---------- 476.09/148.03 The following argument positions are usable: 476.09/148.03 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_4) = {1} 476.09/148.03 476.09/148.03 TcT has computed the following constructor-based matrix 476.09/148.03 interpretation satisfying not(EDA). 476.09/148.03 476.09/148.03 [minus](x1, x2) = [2] 476.09/148.03 476.09/148.03 [0] = [0] 476.09/148.03 476.09/148.03 [s](x1) = [0] 476.09/148.03 476.09/148.03 [plus](x1, x2) = [4] 476.09/148.03 476.09/148.03 [minus^#](x1, x2) = [0] 476.09/148.03 476.09/148.03 [quot^#](x1, x2) = [0] 476.09/148.03 476.09/148.03 [plus^#](x1, x2) = [2] x2 + [0] 476.09/148.03 476.09/148.03 [c_1](x1) = [2] x1 + [0] 476.09/148.03 476.09/148.03 [c_2](x1, x2) = [4] x1 + [1] x2 + [0] 476.09/148.03 476.09/148.03 [c_3](x1) = [3] 476.09/148.03 476.09/148.03 [c_4](x1) = [1] x1 + [0] 476.09/148.03 476.09/148.03 [c_5](x1) = [5] 476.09/148.03 476.09/148.03 The order satisfies the following ordering constraints: 476.09/148.03 476.09/148.03 [minus(x, 0())] = [2] 476.09/148.03 ? [1] x + [0] 476.09/148.03 = [x] 476.09/148.03 476.09/148.03 [minus(s(x), s(y))] = [2] 476.09/148.03 >= [2] 476.09/148.03 = [minus(x, y)] 476.09/148.03 476.09/148.03 [plus(minus(x, s(0())), minus(y, s(s(z))))] = [4] 476.09/148.03 >= [4] 476.09/148.03 = [plus(minus(y, s(s(z))), minus(x, s(0())))] 476.09/148.03 476.09/148.03 [plus(0(), y)] = [4] 476.09/148.03 ? [1] y + [0] 476.09/148.03 = [y] 476.09/148.03 476.09/148.03 [plus(s(x), y)] = [4] 476.09/148.03 > [0] 476.09/148.03 = [s(plus(x, y))] 476.09/148.03 476.09/148.03 [plus(plus(x, s(0())), plus(y, s(s(z))))] = [4] 476.09/148.03 >= [4] 476.09/148.03 = [plus(plus(y, s(s(z))), plus(x, s(0())))] 476.09/148.03 476.09/148.03 [minus^#(s(x), s(y))] = [0] 476.09/148.03 >= [0] 476.09/148.03 = [c_1(minus^#(x, y))] 476.09/148.03 476.09/148.03 [quot^#(s(x), s(y))] = [0] 476.09/148.03 >= [0] 476.09/148.03 = [c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))] 476.09/148.03 476.09/148.03 [plus^#(minus(x, s(0())), minus(y, s(s(z))))] = [4] 476.09/148.03 > [3] 476.09/148.03 = [c_3(plus^#(minus(y, s(s(z))), minus(x, s(0()))))] 476.09/148.03 476.09/148.03 [plus^#(s(x), y)] = [2] y + [0] 476.09/148.03 >= [2] y + [0] 476.09/148.03 = [c_4(plus^#(x, y))] 476.09/148.03 476.09/148.03 [plus^#(plus(x, s(0())), plus(y, s(s(z))))] = [8] 476.09/148.03 > [5] 476.09/148.03 = [c_5(plus^#(plus(y, s(s(z))), plus(x, s(0()))))] 476.09/148.03 476.09/148.03 476.09/148.03 The strictly oriented rules are moved into the weak component. 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 476.09/148.03 , plus^#(s(x), y) -> c_4(plus^#(x, y)) } 476.09/148.03 Weak DPs: 476.09/148.03 { plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_3(plus^#(minus(y, s(s(z))), minus(x, s(0())))) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(plus(y, s(s(z))), plus(x, s(0())))) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 We use the processor 'matrix interpretation of dimension 1' to 476.09/148.03 orient following rules strictly. 476.09/148.03 476.09/148.03 DPs: 476.09/148.03 { 3: plus^#(s(x), y) -> c_4(plus^#(x, y)) 476.09/148.03 , 4: plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_3(plus^#(minus(y, s(s(z))), minus(x, s(0())))) } 476.09/148.03 476.09/148.03 Sub-proof: 476.09/148.03 ---------- 476.09/148.03 The following argument positions are usable: 476.09/148.03 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_4) = {1} 476.09/148.03 476.09/148.03 TcT has computed the following constructor-based matrix 476.09/148.03 interpretation satisfying not(EDA). 476.09/148.03 476.09/148.03 [minus](x1, x2) = [2] 476.09/148.03 476.09/148.03 [0] = [0] 476.09/148.03 476.09/148.03 [s](x1) = [1] x1 + [1] 476.09/148.03 476.09/148.03 [plus](x1, x2) = [0] 476.09/148.03 476.09/148.03 [minus^#](x1, x2) = [0] 476.09/148.03 476.09/148.03 [quot^#](x1, x2) = [0] 476.09/148.03 476.09/148.03 [plus^#](x1, x2) = [4] x1 + [0] 476.09/148.03 476.09/148.03 [c_1](x1) = [2] x1 + [0] 476.09/148.03 476.09/148.03 [c_2](x1, x2) = [1] x1 + [2] x2 + [0] 476.09/148.03 476.09/148.03 [c_3](x1) = [7] 476.09/148.03 476.09/148.03 [c_4](x1) = [1] x1 + [1] 476.09/148.03 476.09/148.03 [c_5](x1) = [0] 476.09/148.03 476.09/148.03 The order satisfies the following ordering constraints: 476.09/148.03 476.09/148.03 [minus(x, 0())] = [2] 476.09/148.03 ? [1] x + [0] 476.09/148.03 = [x] 476.09/148.03 476.09/148.03 [minus(s(x), s(y))] = [2] 476.09/148.03 >= [2] 476.09/148.03 = [minus(x, y)] 476.09/148.03 476.09/148.03 [plus(minus(x, s(0())), minus(y, s(s(z))))] = [0] 476.09/148.03 >= [0] 476.09/148.03 = [plus(minus(y, s(s(z))), minus(x, s(0())))] 476.09/148.03 476.09/148.03 [plus(0(), y)] = [0] 476.09/148.03 ? [1] y + [0] 476.09/148.03 = [y] 476.09/148.03 476.09/148.03 [plus(s(x), y)] = [0] 476.09/148.03 ? [1] 476.09/148.03 = [s(plus(x, y))] 476.09/148.03 476.09/148.03 [plus(plus(x, s(0())), plus(y, s(s(z))))] = [0] 476.09/148.03 >= [0] 476.09/148.03 = [plus(plus(y, s(s(z))), plus(x, s(0())))] 476.09/148.03 476.09/148.03 [minus^#(s(x), s(y))] = [0] 476.09/148.03 >= [0] 476.09/148.03 = [c_1(minus^#(x, y))] 476.09/148.03 476.09/148.03 [quot^#(s(x), s(y))] = [0] 476.09/148.03 >= [0] 476.09/148.03 = [c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))] 476.09/148.03 476.09/148.03 [plus^#(minus(x, s(0())), minus(y, s(s(z))))] = [8] 476.09/148.03 > [7] 476.09/148.03 = [c_3(plus^#(minus(y, s(s(z))), minus(x, s(0()))))] 476.09/148.03 476.09/148.03 [plus^#(s(x), y)] = [4] x + [4] 476.09/148.03 > [4] x + [1] 476.09/148.03 = [c_4(plus^#(x, y))] 476.09/148.03 476.09/148.03 [plus^#(plus(x, s(0())), plus(y, s(s(z))))] = [0] 476.09/148.03 >= [0] 476.09/148.03 = [c_5(plus^#(plus(y, s(s(z))), plus(x, s(0()))))] 476.09/148.03 476.09/148.03 476.09/148.03 The strictly oriented rules are moved into the weak component. 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 476.09/148.03 Weak DPs: 476.09/148.03 { plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_3(plus^#(minus(y, s(s(z))), minus(x, s(0())))) 476.09/148.03 , plus^#(s(x), y) -> c_4(plus^#(x, y)) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(plus(y, s(s(z))), plus(x, s(0())))) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 The following weak DPs constitute a sub-graph of the DG that is 476.09/148.03 closed under successors. The DPs are removed. 476.09/148.03 476.09/148.03 { plus^#(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 c_3(plus^#(minus(y, s(s(z))), minus(x, s(0())))) 476.09/148.03 , plus^#(s(x), y) -> c_4(plus^#(x, y)) 476.09/148.03 , plus^#(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 c_5(plus^#(plus(y, s(s(z))), plus(x, s(0())))) } 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) 476.09/148.03 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 476.09/148.03 plus(minus(y, s(s(z))), minus(x, s(0()))) 476.09/148.03 , plus(0(), y) -> y 476.09/148.03 , plus(s(x), y) -> s(plus(x, y)) 476.09/148.03 , plus(plus(x, s(0())), plus(y, s(s(z)))) -> 476.09/148.03 plus(plus(y, s(s(z))), plus(x, s(0()))) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 We replace rewrite rules by usable rules: 476.09/148.03 476.09/148.03 Weak Usable Rules: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) } 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(n^2)). 476.09/148.03 476.09/148.03 Strict DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(n^2)) 476.09/148.03 476.09/148.03 We use the processor 'Small Polynomial Path Order (PS,2-bounded)' 476.09/148.03 to orient following rules strictly. 476.09/148.03 476.09/148.03 DPs: 476.09/148.03 { 1: minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , 2: quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 476.09/148.03 Trs: { minus(s(x), s(y)) -> minus(x, y) } 476.09/148.03 476.09/148.03 Sub-proof: 476.09/148.03 ---------- 476.09/148.03 The input was oriented with the instance of 'Small Polynomial Path 476.09/148.03 Order (PS,2-bounded)' as induced by the safe mapping 476.09/148.03 476.09/148.03 safe(minus) = {}, safe(0) = {}, safe(s) = {1}, safe(plus) = {}, 476.09/148.03 safe(minus^#) = {}, safe(quot^#) = {}, safe(plus^#) = {}, 476.09/148.03 safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(c_4) = {}, 476.09/148.03 safe(c_5) = {} 476.09/148.03 476.09/148.03 and precedence 476.09/148.03 476.09/148.03 minus > minus^#, quot^# > minus^#, minus ~ quot^# . 476.09/148.03 476.09/148.03 Following symbols are considered recursive: 476.09/148.03 476.09/148.03 {minus^#, quot^#} 476.09/148.03 476.09/148.03 The recursion depth is 2. 476.09/148.03 476.09/148.03 Further, following argument filtering is employed: 476.09/148.03 476.09/148.03 pi(minus) = 1, pi(0) = [], pi(s) = [1], pi(plus) = [], 476.09/148.03 pi(minus^#) = [1, 2], pi(quot^#) = [1, 2], pi(plus^#) = [], 476.09/148.03 pi(c_1) = [1], pi(c_2) = [1, 2], pi(c_3) = [], pi(c_4) = [], 476.09/148.03 pi(c_5) = [] 476.09/148.03 476.09/148.03 Usable defined function symbols are a subset of: 476.09/148.03 476.09/148.03 {minus, minus^#, quot^#, plus^#} 476.09/148.03 476.09/148.03 For your convenience, here are the satisfied ordering constraints: 476.09/148.03 476.09/148.03 pi(minus^#(s(x), s(y))) = minus^#(s(; x), s(; y);) 476.09/148.03 > c_1(minus^#(x, y;);) 476.09/148.03 = pi(c_1(minus^#(x, y))) 476.09/148.03 476.09/148.03 pi(quot^#(s(x), s(y))) = quot^#(s(; x), s(; y);) 476.09/148.03 > c_2(quot^#(x, s(; y);), minus^#(x, y;);) 476.09/148.03 = pi(c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))) 476.09/148.03 476.09/148.03 pi(minus(x, 0())) = x 476.09/148.03 >= x 476.09/148.03 = pi(x) 476.09/148.03 476.09/148.03 pi(minus(s(x), s(y))) = s(; x) 476.09/148.03 > x 476.09/148.03 = pi(minus(x, y)) 476.09/148.03 476.09/148.03 476.09/148.03 The strictly oriented rules are moved into the weak component. 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(1)). 476.09/148.03 476.09/148.03 Weak DPs: 476.09/148.03 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(1)) 476.09/148.03 476.09/148.03 The following weak DPs constitute a sub-graph of the DG that is 476.09/148.03 closed under successors. The DPs are removed. 476.09/148.03 476.09/148.03 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 476.09/148.03 , quot^#(s(x), s(y)) -> 476.09/148.03 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(1)). 476.09/148.03 476.09/148.03 Weak Trs: 476.09/148.03 { minus(x, 0()) -> x 476.09/148.03 , minus(s(x), s(y)) -> minus(x, y) } 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(1)) 476.09/148.03 476.09/148.03 No rule is usable, rules are removed from the input problem. 476.09/148.03 476.09/148.03 We are left with following problem, upon which TcT provides the 476.09/148.03 certificate YES(O(1),O(1)). 476.09/148.03 476.09/148.03 Rules: Empty 476.09/148.03 Obligation: 476.09/148.03 innermost runtime complexity 476.09/148.03 Answer: 476.09/148.03 YES(O(1),O(1)) 476.09/148.03 476.09/148.03 Empty rules are trivially bounded 476.09/148.03 476.09/148.03 Hurray, we answered YES(O(1),O(n^2)) 476.67/148.58 EOF