MAYBE

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

Strict Trs:
  { incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), incr(L))
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, adx(L)))
  , nats() -> adx(zeros())
  , zeros() -> cons(0(), zeros())
  , head(cons(X, L)) -> X
  , tail(cons(X, L)) -> L }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { incr^#(nil()) -> c_1()
  , incr^#(cons(X, L)) -> c_2(incr^#(L))
  , adx^#(nil()) -> c_3()
  , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L))
  , nats^#() -> c_5(adx^#(zeros()), zeros^#())
  , zeros^#() -> c_6(zeros^#())
  , head^#(cons(X, L)) -> c_7()
  , tail^#(cons(X, L)) -> c_8() }

and mark the set of starting terms.

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

Strict DPs:
  { incr^#(nil()) -> c_1()
  , incr^#(cons(X, L)) -> c_2(incr^#(L))
  , adx^#(nil()) -> c_3()
  , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L))
  , nats^#() -> c_5(adx^#(zeros()), zeros^#())
  , zeros^#() -> c_6(zeros^#())
  , head^#(cons(X, L)) -> c_7()
  , tail^#(cons(X, L)) -> c_8() }
Weak Trs:
  { incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), incr(L))
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, adx(L)))
  , nats() -> adx(zeros())
  , zeros() -> cons(0(), zeros())
  , head(cons(X, L)) -> X
  , tail(cons(X, L)) -> L }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {1,3,7,8} by applications
of Pre({1,3,7,8}) = {2,4,5}. Here rules are labeled as follows:

  DPs:
    { 1: incr^#(nil()) -> c_1()
    , 2: incr^#(cons(X, L)) -> c_2(incr^#(L))
    , 3: adx^#(nil()) -> c_3()
    , 4: adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L))
    , 5: nats^#() -> c_5(adx^#(zeros()), zeros^#())
    , 6: zeros^#() -> c_6(zeros^#())
    , 7: head^#(cons(X, L)) -> c_7()
    , 8: tail^#(cons(X, L)) -> c_8() }

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

Strict DPs:
  { incr^#(cons(X, L)) -> c_2(incr^#(L))
  , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L))
  , nats^#() -> c_5(adx^#(zeros()), zeros^#())
  , zeros^#() -> c_6(zeros^#()) }
Weak DPs:
  { incr^#(nil()) -> c_1()
  , adx^#(nil()) -> c_3()
  , head^#(cons(X, L)) -> c_7()
  , tail^#(cons(X, L)) -> c_8() }
Weak Trs:
  { incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), incr(L))
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, adx(L)))
  , nats() -> adx(zeros())
  , zeros() -> cons(0(), zeros())
  , head(cons(X, L)) -> X
  , tail(cons(X, L)) -> L }
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.

{ incr^#(nil()) -> c_1()
, adx^#(nil()) -> c_3()
, head^#(cons(X, L)) -> c_7()
, tail^#(cons(X, L)) -> c_8() }

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

Strict DPs:
  { incr^#(cons(X, L)) -> c_2(incr^#(L))
  , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L))
  , nats^#() -> c_5(adx^#(zeros()), zeros^#())
  , zeros^#() -> c_6(zeros^#()) }
Weak Trs:
  { incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), incr(L))
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, adx(L)))
  , nats() -> adx(zeros())
  , zeros() -> cons(0(), zeros())
  , head(cons(X, L)) -> X
  , tail(cons(X, L)) -> L }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { incr(nil()) -> nil()
    , incr(cons(X, L)) -> cons(s(X), incr(L))
    , adx(nil()) -> nil()
    , adx(cons(X, L)) -> incr(cons(X, adx(L)))
    , zeros() -> cons(0(), zeros()) }

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

Strict DPs:
  { incr^#(cons(X, L)) -> c_2(incr^#(L))
  , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L))
  , nats^#() -> c_5(adx^#(zeros()), zeros^#())
  , zeros^#() -> c_6(zeros^#()) }
Weak Trs:
  { incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), incr(L))
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, adx(L)))
  , zeros() -> cons(0(), zeros()) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..