MAYBE

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

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

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

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

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

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

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

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

The input cannot be shown compatible

Arrrr..