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 following argument positions are usable: Uargs(c_2) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_6) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [1 0 0] [0] [min](x1, x2) = [0 1 0] x1 + [0] [0 0 1] [0] [0] [0] = [0] [0] [1 0 1] [0] [s](x1) = [0 1 0] x1 + [1] [0 1 1] [1] [1 0 0] [0] [quot](x1, x2) = [0 1 0] x1 + [0] [0 0 1] [0] [0 1 0] [0] [min^#](x1, x2) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_2](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [0 0 1] [1] [quot^#](x1, x2) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [c_4](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [1 1 0] [0] [log^#](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [c_6](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] This order satisfies following ordering constraints: [min(X, 0())] = [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] = [X] [min(s(X), s(Y))] = [1 0 1] [0] [0 1 0] X + [1] [0 1 1] [1] >= [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] = [min(X, Y)] [quot(0(), s(Y))] = [0] [0] [0] >= [0] [0] [0] = [0()] [quot(s(X), s(Y))] = [1 0 1] [0] [0 1 0] X + [1] [0 1 1] [1] >= [1 0 1] [0] [0 1 0] X + [1] [0 1 1] [1] = [s(quot(min(X, Y), s(Y)))] [min^#(s(X), s(Y))] = [0 1 0] [1] [0 0 0] X + [0] [0 0 0] [0] > [0 1 0] [0] [0 0 0] X + [0] [0 0 0] [0] = [c_2(min^#(X, Y))] [quot^#(s(X), s(Y))] = [0 1 1] [2] [0 0 0] X + [0] [0 0 0] [0] > [0 1 1] [1] [0 0 0] X + [0] [0 0 0] [0] = [c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))] [log^#(s(s(X)))] = [1 2 2] [3] [0 0 0] X + [0] [0 0 0] [0] > [1 1 2] [2] [0 0 0] X + [0] [0 0 0] [0] = [c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0()))))] Hurray, we answered YES(?,O(n^3))