YES(?,O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict Trs: { pred(s(x)) -> x , minus(x, s(y)) -> pred(minus(x, y)) , minus(x, 0()) -> x , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We add following dependency tuples: Strict DPs: { pred^#(s(x)) -> c_1() , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y)) , minus^#(x, 0()) -> c_3() , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , quot^#(0(), s(y)) -> c_5() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { pred^#(s(x)) -> c_1() , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y)) , minus^#(x, 0()) -> c_3() , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , quot^#(0(), s(y)) -> c_5() } Weak Trs: { pred(s(x)) -> x , minus(x, s(y)) -> pred(minus(x, y)) , minus(x, 0()) -> x , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We estimate the number of application of {1,3,5} by applications of Pre({1,3,5}) = {2,4}. Here rules are labeled as follows: DPs: { 1: pred^#(s(x)) -> c_1() , 2: minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y)) , 3: minus^#(x, 0()) -> c_3() , 4: quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , 5: quot^#(0(), s(y)) -> c_5() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak DPs: { pred^#(s(x)) -> c_1() , minus^#(x, 0()) -> c_3() , quot^#(0(), s(y)) -> c_5() } Weak Trs: { pred(s(x)) -> x , minus(x, s(y)) -> pred(minus(x, y)) , minus(x, 0()) -> x , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { pred^#(s(x)) -> c_1() , minus^#(x, 0()) -> c_3() , quot^#(0(), s(y)) -> c_5() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { pred(s(x)) -> x , minus(x, s(y)) -> pred(minus(x, y)) , minus(x, 0()) -> x , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { minus^#(x, s(y)) -> c_1(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { pred(s(x)) -> x , minus(x, s(y)) -> pred(minus(x, y)) , minus(x, 0()) -> x , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { pred(s(x)) -> x , minus(x, s(y)) -> pred(minus(x, y)) , minus(x, 0()) -> x } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { minus^#(x, s(y)) -> c_1(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { pred(s(x)) -> x , minus(x, s(y)) -> pred(minus(x, y)) , minus(x, 0()) -> x } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) The input was oriented with the instance of 'Small Polynomial Path Order (PS)' as induced by the safe mapping safe(pred) = {}, safe(s) = {1}, safe(minus) = {}, safe(0) = {}, safe(minus^#) = {}, safe(quot^#) = {}, safe(c_1) = {}, safe(c_2) = {} and precedence minus > pred, minus > minus^#, quot^# > pred, quot^# > minus^#, pred ~ minus^#, minus ~ quot^# . Following symbols are considered recursive: {pred, minus, minus^#, quot^#} The recursion depth is 2. Further, following argument filtering is employed: pi(pred) = 1, pi(s) = [1], pi(minus) = 1, pi(0) = [], pi(minus^#) = [1, 2], pi(quot^#) = [1, 2], pi(c_1) = [1], pi(c_2) = [1, 2] Usable defined function symbols are a subset of: {pred, minus, minus^#, quot^#} For your convenience, here are the satisfied ordering constraints: pi(minus^#(x, s(y))) = minus^#(x, s(; y);) > c_1(minus^#(x, y;);) = pi(c_1(minus^#(x, y))) pi(quot^#(s(x), s(y))) = quot^#(s(; x), s(; y);) > c_2(quot^#(x, s(; y);), minus^#(x, y;);) = pi(c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))) pi(pred(s(x))) = s(; x) > x = pi(x) pi(minus(x, s(y))) = x >= x = pi(pred(minus(x, y))) pi(minus(x, 0())) = x >= x = pi(x) Hurray, we answered YES(?,O(n^2))