YES(?,O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict Trs: { a__minus(X1, X2) -> minus(X1, X2) , a__minus(0(), Y) -> 0() , a__minus(s(X), s(Y)) -> a__minus(X, Y) , a__geq(X1, X2) -> geq(X1, X2) , a__geq(X, 0()) -> true() , a__geq(0(), s(Y)) -> false() , a__geq(s(X), s(Y)) -> a__geq(X, Y) , a__div(X1, X2) -> div(X1, X2) , a__div(0(), s(Y)) -> 0() , a__div(s(X), s(Y)) -> a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , mark(0()) -> 0() , mark(s(X)) -> s(mark(X)) , mark(true()) -> true() , mark(false()) -> false() , mark(div(X1, X2)) -> a__div(mark(X1), X2) , mark(minus(X1, X2)) -> a__minus(X1, X2) , mark(geq(X1, X2)) -> a__geq(X1, X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We add following dependency tuples: Strict DPs: { a__minus^#(X1, X2) -> c_1() , a__minus^#(0(), Y) -> c_2() , a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) , a__geq^#(X1, X2) -> c_4() , a__geq^#(X, 0()) -> c_5() , a__geq^#(0(), s(Y)) -> c_6() , a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) , a__div^#(X1, X2) -> c_8() , a__div^#(0(), s(Y)) -> c_9() , a__div^#(s(X), s(Y)) -> c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), a__geq^#(X, Y)) , a__if^#(X1, X2, X3) -> c_11() , a__if^#(true(), X, Y) -> c_12(mark^#(X)) , a__if^#(false(), X, Y) -> c_13(mark^#(Y)) , mark^#(0()) -> c_14() , mark^#(s(X)) -> c_15(mark^#(X)) , mark^#(true()) -> c_16() , mark^#(false()) -> c_17() , mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1)) , mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) , mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) , mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) } 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: { a__minus^#(X1, X2) -> c_1() , a__minus^#(0(), Y) -> c_2() , a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) , a__geq^#(X1, X2) -> c_4() , a__geq^#(X, 0()) -> c_5() , a__geq^#(0(), s(Y)) -> c_6() , a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) , a__div^#(X1, X2) -> c_8() , a__div^#(0(), s(Y)) -> c_9() , a__div^#(s(X), s(Y)) -> c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), a__geq^#(X, Y)) , a__if^#(X1, X2, X3) -> c_11() , a__if^#(true(), X, Y) -> c_12(mark^#(X)) , a__if^#(false(), X, Y) -> c_13(mark^#(Y)) , mark^#(0()) -> c_14() , mark^#(s(X)) -> c_15(mark^#(X)) , mark^#(true()) -> c_16() , mark^#(false()) -> c_17() , mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1)) , mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) , mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) , mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) } Weak Trs: { a__minus(X1, X2) -> minus(X1, X2) , a__minus(0(), Y) -> 0() , a__minus(s(X), s(Y)) -> a__minus(X, Y) , a__geq(X1, X2) -> geq(X1, X2) , a__geq(X, 0()) -> true() , a__geq(0(), s(Y)) -> false() , a__geq(s(X), s(Y)) -> a__geq(X, Y) , a__div(X1, X2) -> div(X1, X2) , a__div(0(), s(Y)) -> 0() , a__div(s(X), s(Y)) -> a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , mark(0()) -> 0() , mark(s(X)) -> s(mark(X)) , mark(true()) -> true() , mark(false()) -> false() , mark(div(X1, X2)) -> a__div(mark(X1), X2) , mark(minus(X1, X2)) -> a__minus(X1, X2) , mark(geq(X1, X2)) -> a__geq(X1, X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We estimate the number of application of {1,2,4,5,6,8,9,11,14,16,17} by applications of Pre({1,2,4,5,6,8,9,11,14,16,17}) = {3,7,10,12,13,15,18,19,20,21}. Here rules are labeled as follows: DPs: { 1: a__minus^#(X1, X2) -> c_1() , 2: a__minus^#(0(), Y) -> c_2() , 3: a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) , 4: a__geq^#(X1, X2) -> c_4() , 5: a__geq^#(X, 0()) -> c_5() , 6: a__geq^#(0(), s(Y)) -> c_6() , 7: a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) , 8: a__div^#(X1, X2) -> c_8() , 9: a__div^#(0(), s(Y)) -> c_9() , 10: a__div^#(s(X), s(Y)) -> c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), a__geq^#(X, Y)) , 11: a__if^#(X1, X2, X3) -> c_11() , 12: a__if^#(true(), X, Y) -> c_12(mark^#(X)) , 13: a__if^#(false(), X, Y) -> c_13(mark^#(Y)) , 14: mark^#(0()) -> c_14() , 15: mark^#(s(X)) -> c_15(mark^#(X)) , 16: mark^#(true()) -> c_16() , 17: mark^#(false()) -> c_17() , 18: mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1)) , 19: mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) , 20: mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) , 21: mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) , a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) , a__div^#(s(X), s(Y)) -> c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), a__geq^#(X, Y)) , a__if^#(true(), X, Y) -> c_12(mark^#(X)) , a__if^#(false(), X, Y) -> c_13(mark^#(Y)) , mark^#(s(X)) -> c_15(mark^#(X)) , mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1)) , mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) , mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) , mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) } Weak DPs: { a__minus^#(X1, X2) -> c_1() , a__minus^#(0(), Y) -> c_2() , a__geq^#(X1, X2) -> c_4() , a__geq^#(X, 0()) -> c_5() , a__geq^#(0(), s(Y)) -> c_6() , a__div^#(X1, X2) -> c_8() , a__div^#(0(), s(Y)) -> c_9() , a__if^#(X1, X2, X3) -> c_11() , mark^#(0()) -> c_14() , mark^#(true()) -> c_16() , mark^#(false()) -> c_17() } Weak Trs: { a__minus(X1, X2) -> minus(X1, X2) , a__minus(0(), Y) -> 0() , a__minus(s(X), s(Y)) -> a__minus(X, Y) , a__geq(X1, X2) -> geq(X1, X2) , a__geq(X, 0()) -> true() , a__geq(0(), s(Y)) -> false() , a__geq(s(X), s(Y)) -> a__geq(X, Y) , a__div(X1, X2) -> div(X1, X2) , a__div(0(), s(Y)) -> 0() , a__div(s(X), s(Y)) -> a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , mark(0()) -> 0() , mark(s(X)) -> s(mark(X)) , mark(true()) -> true() , mark(false()) -> false() , mark(div(X1, X2)) -> a__div(mark(X1), X2) , mark(minus(X1, X2)) -> a__minus(X1, X2) , mark(geq(X1, X2)) -> a__geq(X1, X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 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. { a__minus^#(X1, X2) -> c_1() , a__minus^#(0(), Y) -> c_2() , a__geq^#(X1, X2) -> c_4() , a__geq^#(X, 0()) -> c_5() , a__geq^#(0(), s(Y)) -> c_6() , a__div^#(X1, X2) -> c_8() , a__div^#(0(), s(Y)) -> c_9() , a__if^#(X1, X2, X3) -> c_11() , mark^#(0()) -> c_14() , mark^#(true()) -> c_16() , mark^#(false()) -> c_17() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y)) , a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y)) , a__div^#(s(X), s(Y)) -> c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), a__geq^#(X, Y)) , a__if^#(true(), X, Y) -> c_12(mark^#(X)) , a__if^#(false(), X, Y) -> c_13(mark^#(Y)) , mark^#(s(X)) -> c_15(mark^#(X)) , mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1)) , mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2)) , mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2)) , mark^#(if(X1, X2, X3)) -> c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) } Weak Trs: { a__minus(X1, X2) -> minus(X1, X2) , a__minus(0(), Y) -> 0() , a__minus(s(X), s(Y)) -> a__minus(X, Y) , a__geq(X1, X2) -> geq(X1, X2) , a__geq(X, 0()) -> true() , a__geq(0(), s(Y)) -> false() , a__geq(s(X), s(Y)) -> a__geq(X, Y) , a__div(X1, X2) -> div(X1, X2) , a__div(0(), s(Y)) -> 0() , a__div(s(X), s(Y)) -> a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , mark(0()) -> 0() , mark(s(X)) -> s(mark(X)) , mark(true()) -> true() , mark(false()) -> false() , mark(div(X1, X2)) -> a__div(mark(X1), X2) , mark(minus(X1, X2)) -> a__minus(X1, X2) , mark(geq(X1, X2)) -> a__geq(X1, X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) The following argument positions are usable: Uargs(c_3) = {1}, Uargs(c_7) = {1}, Uargs(c_10) = {1, 2}, Uargs(c_12) = {1}, Uargs(c_13) = {1}, Uargs(c_15) = {1}, Uargs(c_18) = {1, 2}, Uargs(c_19) = {1}, Uargs(c_20) = {1}, Uargs(c_21) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [a__minus](x1, x2) = [0 1] x1 + [0] [0 0] [0] [0] = [0] [0] [s](x1) = [1 0] x1 + [0] [0 1] [2] [a__geq](x1, x2) = [0 1] x1 + [0] [0 0] [0] [true] = [0] [0] [false] = [0] [0] [a__div](x1, x2) = [1 3] x1 + [0] [0 1] [1] [a__if](x1, x2, x3) = [1 2] x1 + [2 0] x2 + [2 2] x3 + [3] [0 0] [0 1] [0 1] [0] [div](x1, x2) = [1 3] x1 + [0] [0 1] [1] [minus](x1, x2) = [0 1] x1 + [0] [0 0] [0] [mark](x1) = [2 0] x1 + [0] [0 1] [0] [geq](x1, x2) = [0 1] x1 + [0] [0 0] [0] [if](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 2] x3 + [3] [0 0] [0 1] [0 1] [0] [a__minus^#](x1, x2) = [0 1] x1 + [0] [0 0] [0] [c_3](x1) = [1 0] x1 + [1] [0 0] [0] [a__geq^#](x1, x2) = [0 1] x1 + [0] [0 0] [0] [c_7](x1) = [1 0] x1 + [1] [0 0] [0] [a__div^#](x1, x2) = [0 3] x1 + [0] [0 0] [0] [c_10](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [a__if^#](x1, x2, x3) = [2 1] x2 + [2 1] x3 + [2] [0 0] [0 0] [0] [c_12](x1) = [1 0] x1 + [0] [0 0] [0] [mark^#](x1) = [2 1] x1 + [1] [0 1] [1] [c_13](x1) = [1 0] x1 + [0] [0 0] [0] [c_15](x1) = [1 0] x1 + [1] [0 0] [3] [c_18](x1, x2) = [2 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] [c_19](x1) = [2 0] x1 + [0] [0 0] [1] [c_20](x1) = [1 0] x1 + [0] [0 0] [1] [c_21](x1, x2) = [1 0] x1 + [1 3] x2 + [0] [0 0] [0 0] [1] This order satisfies following ordering constraints: [a__minus(X1, X2)] = [0 1] X1 + [0] [0 0] [0] >= [0 1] X1 + [0] [0 0] [0] = [minus(X1, X2)] [a__minus(0(), Y)] = [0] [0] >= [0] [0] = [0()] [a__minus(s(X), s(Y))] = [0 1] X + [2] [0 0] [0] > [0 1] X + [0] [0 0] [0] = [a__minus(X, Y)] [a__geq(X1, X2)] = [0 1] X1 + [0] [0 0] [0] >= [0 1] X1 + [0] [0 0] [0] = [geq(X1, X2)] [a__geq(X, 0())] = [0 1] X + [0] [0 0] [0] >= [0] [0] = [true()] [a__geq(0(), s(Y))] = [0] [0] >= [0] [0] = [false()] [a__geq(s(X), s(Y))] = [0 1] X + [2] [0 0] [0] > [0 1] X + [0] [0 0] [0] = [a__geq(X, Y)] [a__div(X1, X2)] = [1 3] X1 + [0] [0 1] [1] >= [1 3] X1 + [0] [0 1] [1] = [div(X1, X2)] [a__div(0(), s(Y))] = [0] [1] >= [0] [0] = [0()] [a__div(s(X), s(Y))] = [1 3] X + [6] [0 1] [3] > [0 3] X + [3] [0 0] [3] = [a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())] [a__if(X1, X2, X3)] = [1 2] X1 + [2 0] X2 + [2 2] X3 + [3] [0 0] [0 1] [0 1] [0] >= [1 2] X1 + [1 0] X2 + [1 2] X3 + [3] [0 0] [0 1] [0 1] [0] = [if(X1, X2, X3)] [a__if(true(), X, Y)] = [2 2] Y + [2 0] X + [3] [0 1] [0 1] [0] > [2 0] X + [0] [0 1] [0] = [mark(X)] [a__if(false(), X, Y)] = [2 2] Y + [2 0] X + [3] [0 1] [0 1] [0] > [2 0] Y + [0] [0 1] [0] = [mark(Y)] [mark(0())] = [0] [0] >= [0] [0] = [0()] [mark(s(X))] = [2 0] X + [0] [0 1] [2] >= [2 0] X + [0] [0 1] [2] = [s(mark(X))] [mark(true())] = [0] [0] >= [0] [0] = [true()] [mark(false())] = [0] [0] >= [0] [0] = [false()] [mark(div(X1, X2))] = [2 6] X1 + [0] [0 1] [1] >= [2 3] X1 + [0] [0 1] [1] = [a__div(mark(X1), X2)] [mark(minus(X1, X2))] = [0 2] X1 + [0] [0 0] [0] >= [0 1] X1 + [0] [0 0] [0] = [a__minus(X1, X2)] [mark(geq(X1, X2))] = [0 2] X1 + [0] [0 0] [0] >= [0 1] X1 + [0] [0 0] [0] = [a__geq(X1, X2)] [mark(if(X1, X2, X3))] = [2 4] X1 + [2 0] X2 + [2 4] X3 + [6] [0 0] [0 1] [0 1] [0] > [2 2] X1 + [2 0] X2 + [2 2] X3 + [3] [0 0] [0 1] [0 1] [0] = [a__if(mark(X1), X2, X3)] [a__minus^#(s(X), s(Y))] = [0 1] X + [2] [0 0] [0] > [0 1] X + [1] [0 0] [0] = [c_3(a__minus^#(X, Y))] [a__geq^#(s(X), s(Y))] = [0 1] X + [2] [0 0] [0] > [0 1] X + [1] [0 0] [0] = [c_7(a__geq^#(X, Y))] [a__div^#(s(X), s(Y))] = [0 3] X + [6] [0 0] [0] > [0 3] X + [5] [0 0] [0] = [c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), a__geq^#(X, Y))] [a__if^#(true(), X, Y)] = [2 1] Y + [2 1] X + [2] [0 0] [0 0] [0] > [2 1] X + [1] [0 0] [0] = [c_12(mark^#(X))] [a__if^#(false(), X, Y)] = [2 1] Y + [2 1] X + [2] [0 0] [0 0] [0] > [2 1] Y + [1] [0 0] [0] = [c_13(mark^#(Y))] [mark^#(s(X))] = [2 1] X + [3] [0 1] [3] > [2 1] X + [2] [0 0] [3] = [c_15(mark^#(X))] [mark^#(div(X1, X2))] = [2 7] X1 + [2] [0 1] [2] > [2 7] X1 + [1] [0 0] [1] = [c_18(a__div^#(mark(X1), X2), mark^#(X1))] [mark^#(minus(X1, X2))] = [0 2] X1 + [1] [0 0] [1] > [0 2] X1 + [0] [0 0] [1] = [c_19(a__minus^#(X1, X2))] [mark^#(geq(X1, X2))] = [0 2] X1 + [1] [0 0] [1] > [0 1] X1 + [0] [0 0] [1] = [c_20(a__geq^#(X1, X2))] [mark^#(if(X1, X2, X3))] = [2 4] X1 + [2 1] X2 + [2 5] X3 + [7] [0 0] [0 1] [0 1] [1] > [2 4] X1 + [2 1] X2 + [2 1] X3 + [6] [0 0] [0 0] [0 0] [1] = [c_21(a__if^#(mark(X1), X2, X3), mark^#(X1))] Hurray, we answered YES(?,O(n^2))