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