MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

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:
  MAYBE

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 MAYBE.

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:
  MAYBE

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 MAYBE.

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:
  MAYBE

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 MAYBE.

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:
  MAYBE

The input cannot be shown compatible

Arrrr..