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