MAYBE

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

Strict Trs:
  { a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(from(X)) -> a__from(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(0()) -> 0()
  , mark(nil()) -> nil()
  , mark(zWquot(X1, X2)) -> a__zWquot(mark(X1), mark(X2))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(minus(X1, X2)) -> a__minus(mark(X1), mark(X2))
  , mark(quot(X1, X2)) -> a__quot(mark(X1), mark(X2))
  , a__sel(X1, X2) -> sel(X1, X2)
  , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS))
  , a__sel(0(), cons(X, XS)) -> mark(X)
  , a__minus(X1, X2) -> minus(X1, X2)
  , a__minus(X, 0()) -> 0()
  , a__minus(s(X), s(Y)) -> a__minus(mark(X), mark(Y))
  , a__quot(X1, X2) -> quot(X1, X2)
  , a__quot(s(X), s(Y)) ->
    s(a__quot(a__minus(mark(X), mark(Y)), s(mark(Y))))
  , a__quot(0(), s(Y)) -> 0()
  , a__zWquot(X1, X2) -> zWquot(X1, X2)
  , a__zWquot(XS, nil()) -> nil()
  , a__zWquot(cons(X, XS), cons(Y, YS)) ->
    cons(a__quot(mark(X), mark(Y)), zWquot(XS, YS))
  , a__zWquot(nil(), XS) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { a__from^#(X) -> c_1(mark^#(X))
  , a__from^#(X) -> c_2()
  , mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
  , mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
  , mark^#(s(X)) -> c_5(mark^#(X))
  , mark^#(0()) -> c_6()
  , mark^#(nil()) -> c_7()
  , mark^#(zWquot(X1, X2)) ->
    c_8(a__zWquot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(sel(X1, X2)) ->
    c_9(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(minus(X1, X2)) ->
    c_10(a__minus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quot(X1, X2)) ->
    c_11(a__quot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , a__zWquot^#(X1, X2) -> c_21()
  , a__zWquot^#(XS, nil()) -> c_22()
  , a__zWquot^#(cons(X, XS), cons(Y, YS)) ->
    c_23(a__quot^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__zWquot^#(nil(), XS) -> c_24()
  , a__sel^#(X1, X2) -> c_12()
  , a__sel^#(s(N), cons(X, XS)) ->
    c_13(a__sel^#(mark(N), mark(XS)), mark^#(N), mark^#(XS))
  , a__sel^#(0(), cons(X, XS)) -> c_14(mark^#(X))
  , a__minus^#(X1, X2) -> c_15()
  , a__minus^#(X, 0()) -> c_16()
  , a__minus^#(s(X), s(Y)) ->
    c_17(a__minus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__quot^#(X1, X2) -> c_18()
  , a__quot^#(s(X), s(Y)) ->
    c_19(a__quot^#(a__minus(mark(X), mark(Y)), s(mark(Y))),
         a__minus^#(mark(X), mark(Y)),
         mark^#(X),
         mark^#(Y),
         mark^#(Y))
  , a__quot^#(0(), s(Y)) -> c_20() }

and mark the set of starting terms.

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

Strict DPs:
  { a__from^#(X) -> c_1(mark^#(X))
  , a__from^#(X) -> c_2()
  , mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
  , mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
  , mark^#(s(X)) -> c_5(mark^#(X))
  , mark^#(0()) -> c_6()
  , mark^#(nil()) -> c_7()
  , mark^#(zWquot(X1, X2)) ->
    c_8(a__zWquot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(sel(X1, X2)) ->
    c_9(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(minus(X1, X2)) ->
    c_10(a__minus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quot(X1, X2)) ->
    c_11(a__quot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , a__zWquot^#(X1, X2) -> c_21()
  , a__zWquot^#(XS, nil()) -> c_22()
  , a__zWquot^#(cons(X, XS), cons(Y, YS)) ->
    c_23(a__quot^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__zWquot^#(nil(), XS) -> c_24()
  , a__sel^#(X1, X2) -> c_12()
  , a__sel^#(s(N), cons(X, XS)) ->
    c_13(a__sel^#(mark(N), mark(XS)), mark^#(N), mark^#(XS))
  , a__sel^#(0(), cons(X, XS)) -> c_14(mark^#(X))
  , a__minus^#(X1, X2) -> c_15()
  , a__minus^#(X, 0()) -> c_16()
  , a__minus^#(s(X), s(Y)) ->
    c_17(a__minus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__quot^#(X1, X2) -> c_18()
  , a__quot^#(s(X), s(Y)) ->
    c_19(a__quot^#(a__minus(mark(X), mark(Y)), s(mark(Y))),
         a__minus^#(mark(X), mark(Y)),
         mark^#(X),
         mark^#(Y),
         mark^#(Y))
  , a__quot^#(0(), s(Y)) -> c_20() }
Weak Trs:
  { a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(from(X)) -> a__from(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(0()) -> 0()
  , mark(nil()) -> nil()
  , mark(zWquot(X1, X2)) -> a__zWquot(mark(X1), mark(X2))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(minus(X1, X2)) -> a__minus(mark(X1), mark(X2))
  , mark(quot(X1, X2)) -> a__quot(mark(X1), mark(X2))
  , a__sel(X1, X2) -> sel(X1, X2)
  , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS))
  , a__sel(0(), cons(X, XS)) -> mark(X)
  , a__minus(X1, X2) -> minus(X1, X2)
  , a__minus(X, 0()) -> 0()
  , a__minus(s(X), s(Y)) -> a__minus(mark(X), mark(Y))
  , a__quot(X1, X2) -> quot(X1, X2)
  , a__quot(s(X), s(Y)) ->
    s(a__quot(a__minus(mark(X), mark(Y)), s(mark(Y))))
  , a__quot(0(), s(Y)) -> 0()
  , a__zWquot(X1, X2) -> zWquot(X1, X2)
  , a__zWquot(XS, nil()) -> nil()
  , a__zWquot(cons(X, XS), cons(Y, YS)) ->
    cons(a__quot(mark(X), mark(Y)), zWquot(XS, YS))
  , a__zWquot(nil(), XS) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{2,6,7,12,13,15,16,19,20,22,24} by applications of
Pre({2,6,7,12,13,15,16,19,20,22,24}) =
{1,3,4,5,8,9,10,11,14,17,18,21,23}. Here rules are labeled as
follows:

  DPs:
    { 1: a__from^#(X) -> c_1(mark^#(X))
    , 2: a__from^#(X) -> c_2()
    , 3: mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
    , 4: mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
    , 5: mark^#(s(X)) -> c_5(mark^#(X))
    , 6: mark^#(0()) -> c_6()
    , 7: mark^#(nil()) -> c_7()
    , 8: mark^#(zWquot(X1, X2)) ->
         c_8(a__zWquot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 9: mark^#(sel(X1, X2)) ->
         c_9(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 10: mark^#(minus(X1, X2)) ->
          c_10(a__minus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 11: mark^#(quot(X1, X2)) ->
          c_11(a__quot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 12: a__zWquot^#(X1, X2) -> c_21()
    , 13: a__zWquot^#(XS, nil()) -> c_22()
    , 14: a__zWquot^#(cons(X, XS), cons(Y, YS)) ->
          c_23(a__quot^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
    , 15: a__zWquot^#(nil(), XS) -> c_24()
    , 16: a__sel^#(X1, X2) -> c_12()
    , 17: a__sel^#(s(N), cons(X, XS)) ->
          c_13(a__sel^#(mark(N), mark(XS)), mark^#(N), mark^#(XS))
    , 18: a__sel^#(0(), cons(X, XS)) -> c_14(mark^#(X))
    , 19: a__minus^#(X1, X2) -> c_15()
    , 20: a__minus^#(X, 0()) -> c_16()
    , 21: a__minus^#(s(X), s(Y)) ->
          c_17(a__minus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
    , 22: a__quot^#(X1, X2) -> c_18()
    , 23: a__quot^#(s(X), s(Y)) ->
          c_19(a__quot^#(a__minus(mark(X), mark(Y)), s(mark(Y))),
               a__minus^#(mark(X), mark(Y)),
               mark^#(X),
               mark^#(Y),
               mark^#(Y))
    , 24: a__quot^#(0(), s(Y)) -> c_20() }

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

Strict DPs:
  { a__from^#(X) -> c_1(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
  , mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
  , mark^#(s(X)) -> c_5(mark^#(X))
  , mark^#(zWquot(X1, X2)) ->
    c_8(a__zWquot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(sel(X1, X2)) ->
    c_9(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(minus(X1, X2)) ->
    c_10(a__minus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quot(X1, X2)) ->
    c_11(a__quot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , a__zWquot^#(cons(X, XS), cons(Y, YS)) ->
    c_23(a__quot^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__sel^#(s(N), cons(X, XS)) ->
    c_13(a__sel^#(mark(N), mark(XS)), mark^#(N), mark^#(XS))
  , a__sel^#(0(), cons(X, XS)) -> c_14(mark^#(X))
  , a__minus^#(s(X), s(Y)) ->
    c_17(a__minus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__quot^#(s(X), s(Y)) ->
    c_19(a__quot^#(a__minus(mark(X), mark(Y)), s(mark(Y))),
         a__minus^#(mark(X), mark(Y)),
         mark^#(X),
         mark^#(Y),
         mark^#(Y)) }
Weak DPs:
  { a__from^#(X) -> c_2()
  , mark^#(0()) -> c_6()
  , mark^#(nil()) -> c_7()
  , a__zWquot^#(X1, X2) -> c_21()
  , a__zWquot^#(XS, nil()) -> c_22()
  , a__zWquot^#(nil(), XS) -> c_24()
  , a__sel^#(X1, X2) -> c_12()
  , a__minus^#(X1, X2) -> c_15()
  , a__minus^#(X, 0()) -> c_16()
  , a__quot^#(X1, X2) -> c_18()
  , a__quot^#(0(), s(Y)) -> c_20() }
Weak Trs:
  { a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(from(X)) -> a__from(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(0()) -> 0()
  , mark(nil()) -> nil()
  , mark(zWquot(X1, X2)) -> a__zWquot(mark(X1), mark(X2))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(minus(X1, X2)) -> a__minus(mark(X1), mark(X2))
  , mark(quot(X1, X2)) -> a__quot(mark(X1), mark(X2))
  , a__sel(X1, X2) -> sel(X1, X2)
  , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS))
  , a__sel(0(), cons(X, XS)) -> mark(X)
  , a__minus(X1, X2) -> minus(X1, X2)
  , a__minus(X, 0()) -> 0()
  , a__minus(s(X), s(Y)) -> a__minus(mark(X), mark(Y))
  , a__quot(X1, X2) -> quot(X1, X2)
  , a__quot(s(X), s(Y)) ->
    s(a__quot(a__minus(mark(X), mark(Y)), s(mark(Y))))
  , a__quot(0(), s(Y)) -> 0()
  , a__zWquot(X1, X2) -> zWquot(X1, X2)
  , a__zWquot(XS, nil()) -> nil()
  , a__zWquot(cons(X, XS), cons(Y, YS)) ->
    cons(a__quot(mark(X), mark(Y)), zWquot(XS, YS))
  , a__zWquot(nil(), XS) -> nil() }
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__from^#(X) -> c_2()
, mark^#(0()) -> c_6()
, mark^#(nil()) -> c_7()
, a__zWquot^#(X1, X2) -> c_21()
, a__zWquot^#(XS, nil()) -> c_22()
, a__zWquot^#(nil(), XS) -> c_24()
, a__sel^#(X1, X2) -> c_12()
, a__minus^#(X1, X2) -> c_15()
, a__minus^#(X, 0()) -> c_16()
, a__quot^#(X1, X2) -> c_18()
, a__quot^#(0(), s(Y)) -> c_20() }

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

Strict DPs:
  { a__from^#(X) -> c_1(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
  , mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
  , mark^#(s(X)) -> c_5(mark^#(X))
  , mark^#(zWquot(X1, X2)) ->
    c_8(a__zWquot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(sel(X1, X2)) ->
    c_9(a__sel^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(minus(X1, X2)) ->
    c_10(a__minus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(quot(X1, X2)) ->
    c_11(a__quot^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , a__zWquot^#(cons(X, XS), cons(Y, YS)) ->
    c_23(a__quot^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__sel^#(s(N), cons(X, XS)) ->
    c_13(a__sel^#(mark(N), mark(XS)), mark^#(N), mark^#(XS))
  , a__sel^#(0(), cons(X, XS)) -> c_14(mark^#(X))
  , a__minus^#(s(X), s(Y)) ->
    c_17(a__minus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__quot^#(s(X), s(Y)) ->
    c_19(a__quot^#(a__minus(mark(X), mark(Y)), s(mark(Y))),
         a__minus^#(mark(X), mark(Y)),
         mark^#(X),
         mark^#(Y),
         mark^#(Y)) }
Weak Trs:
  { a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(from(X)) -> a__from(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(0()) -> 0()
  , mark(nil()) -> nil()
  , mark(zWquot(X1, X2)) -> a__zWquot(mark(X1), mark(X2))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(minus(X1, X2)) -> a__minus(mark(X1), mark(X2))
  , mark(quot(X1, X2)) -> a__quot(mark(X1), mark(X2))
  , a__sel(X1, X2) -> sel(X1, X2)
  , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS))
  , a__sel(0(), cons(X, XS)) -> mark(X)
  , a__minus(X1, X2) -> minus(X1, X2)
  , a__minus(X, 0()) -> 0()
  , a__minus(s(X), s(Y)) -> a__minus(mark(X), mark(Y))
  , a__quot(X1, X2) -> quot(X1, X2)
  , a__quot(s(X), s(Y)) ->
    s(a__quot(a__minus(mark(X), mark(Y)), s(mark(Y))))
  , a__quot(0(), s(Y)) -> 0()
  , a__zWquot(X1, X2) -> zWquot(X1, X2)
  , a__zWquot(XS, nil()) -> nil()
  , a__zWquot(cons(X, XS), cons(Y, YS)) ->
    cons(a__quot(mark(X), mark(Y)), zWquot(XS, YS))
  , a__zWquot(nil(), XS) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..