MAYBE

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

Strict Trs:
  { nats() -> adx(zeros())
  , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
  , zeros() -> cons(0(), zeros())
  , incr(cons(X, Y)) -> cons(s(X), incr(Y))
  , hd(cons(X, Y)) -> X
  , tl(cons(X, Y)) -> Y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { nats^#() -> c_1(adx^#(zeros()), zeros^#())
  , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
  , zeros^#() -> c_3(zeros^#())
  , incr^#(cons(X, Y)) -> c_4(incr^#(Y))
  , hd^#(cons(X, Y)) -> c_5()
  , tl^#(cons(X, Y)) -> c_6() }

and mark the set of starting terms.

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

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

We estimate the number of application of {5,6} by applications of
Pre({5,6}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: nats^#() -> c_1(adx^#(zeros()), zeros^#())
    , 2: adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
    , 3: zeros^#() -> c_3(zeros^#())
    , 4: incr^#(cons(X, Y)) -> c_4(incr^#(Y))
    , 5: hd^#(cons(X, Y)) -> c_5()
    , 6: tl^#(cons(X, Y)) -> c_6() }

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

Strict DPs:
  { nats^#() -> c_1(adx^#(zeros()), zeros^#())
  , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
  , zeros^#() -> c_3(zeros^#())
  , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
Weak DPs:
  { hd^#(cons(X, Y)) -> c_5()
  , tl^#(cons(X, Y)) -> c_6() }
Weak Trs:
  { nats() -> adx(zeros())
  , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
  , zeros() -> cons(0(), zeros())
  , incr(cons(X, Y)) -> cons(s(X), incr(Y))
  , hd(cons(X, Y)) -> X
  , tl(cons(X, Y)) -> 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.

{ hd^#(cons(X, Y)) -> c_5()
, tl^#(cons(X, Y)) -> c_6() }

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

Strict DPs:
  { nats^#() -> c_1(adx^#(zeros()), zeros^#())
  , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y))
  , zeros^#() -> c_3(zeros^#())
  , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) }
Weak Trs:
  { nats() -> adx(zeros())
  , adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
  , zeros() -> cons(0(), zeros())
  , incr(cons(X, Y)) -> cons(s(X), incr(Y))
  , hd(cons(X, Y)) -> X
  , tl(cons(X, Y)) -> Y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

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

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

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

The input cannot be shown compatible

Arrrr..