MAYBE

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

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

We add following dependency tuples:

Strict DPs:
  { nats^#() -> c_1(adx^#(zeros()), zeros^#())
  , adx^#(X) -> c_2()
  , adx^#(cons(X, Y)) ->
    c_3(incr^#(cons(activate(X), n__adx(activate(Y)))),
        activate^#(X),
        activate^#(Y))
  , zeros^#() -> c_4()
  , zeros^#() -> c_5()
  , incr^#(X) -> c_6()
  , incr^#(cons(X, Y)) -> c_7(activate^#(X), activate^#(Y))
  , activate^#(X) -> c_8()
  , activate^#(n__0()) -> c_9(0^#())
  , activate^#(n__zeros()) -> c_10(zeros^#())
  , activate^#(n__s(X)) -> c_11(s^#(X))
  , activate^#(n__incr(X)) ->
    c_12(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_13(adx^#(activate(X)), activate^#(X))
  , 0^#() -> c_16()
  , s^#(X) -> c_17()
  , hd^#(cons(X, Y)) -> c_14(activate^#(X))
  , tl^#(cons(X, Y)) -> c_15(activate^#(Y)) }

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^#(X) -> c_2()
  , adx^#(cons(X, Y)) ->
    c_3(incr^#(cons(activate(X), n__adx(activate(Y)))),
        activate^#(X),
        activate^#(Y))
  , zeros^#() -> c_4()
  , zeros^#() -> c_5()
  , incr^#(X) -> c_6()
  , incr^#(cons(X, Y)) -> c_7(activate^#(X), activate^#(Y))
  , activate^#(X) -> c_8()
  , activate^#(n__0()) -> c_9(0^#())
  , activate^#(n__zeros()) -> c_10(zeros^#())
  , activate^#(n__s(X)) -> c_11(s^#(X))
  , activate^#(n__incr(X)) ->
    c_12(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_13(adx^#(activate(X)), activate^#(X))
  , 0^#() -> c_16()
  , s^#(X) -> c_17()
  , hd^#(cons(X, Y)) -> c_14(activate^#(X))
  , tl^#(cons(X, Y)) -> c_15(activate^#(Y)) }
Weak Trs:
  { nats() -> adx(zeros())
  , adx(X) -> n__adx(X)
  , adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y))))
  , zeros() -> cons(n__0(), n__zeros())
  , zeros() -> n__zeros()
  , incr(X) -> n__incr(X)
  , incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__zeros()) -> zeros()
  , activate(n__s(X)) -> s(X)
  , activate(n__incr(X)) -> incr(activate(X))
  , activate(n__adx(X)) -> adx(activate(X))
  , hd(cons(X, Y)) -> activate(X)
  , tl(cons(X, Y)) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: nats^#() -> c_1(adx^#(zeros()), zeros^#())
    , 2: adx^#(X) -> c_2()
    , 3: adx^#(cons(X, Y)) ->
         c_3(incr^#(cons(activate(X), n__adx(activate(Y)))),
             activate^#(X),
             activate^#(Y))
    , 4: zeros^#() -> c_4()
    , 5: zeros^#() -> c_5()
    , 6: incr^#(X) -> c_6()
    , 7: incr^#(cons(X, Y)) -> c_7(activate^#(X), activate^#(Y))
    , 8: activate^#(X) -> c_8()
    , 9: activate^#(n__0()) -> c_9(0^#())
    , 10: activate^#(n__zeros()) -> c_10(zeros^#())
    , 11: activate^#(n__s(X)) -> c_11(s^#(X))
    , 12: activate^#(n__incr(X)) ->
          c_12(incr^#(activate(X)), activate^#(X))
    , 13: activate^#(n__adx(X)) ->
          c_13(adx^#(activate(X)), activate^#(X))
    , 14: 0^#() -> c_16()
    , 15: s^#(X) -> c_17()
    , 16: hd^#(cons(X, Y)) -> c_14(activate^#(X))
    , 17: tl^#(cons(X, Y)) -> c_15(activate^#(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_3(incr^#(cons(activate(X), n__adx(activate(Y)))),
        activate^#(X),
        activate^#(Y))
  , incr^#(cons(X, Y)) -> c_7(activate^#(X), activate^#(Y))
  , activate^#(n__0()) -> c_9(0^#())
  , activate^#(n__zeros()) -> c_10(zeros^#())
  , activate^#(n__s(X)) -> c_11(s^#(X))
  , activate^#(n__incr(X)) ->
    c_12(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_13(adx^#(activate(X)), activate^#(X))
  , hd^#(cons(X, Y)) -> c_14(activate^#(X))
  , tl^#(cons(X, Y)) -> c_15(activate^#(Y)) }
Weak DPs:
  { adx^#(X) -> c_2()
  , zeros^#() -> c_4()
  , zeros^#() -> c_5()
  , incr^#(X) -> c_6()
  , activate^#(X) -> c_8()
  , 0^#() -> c_16()
  , s^#(X) -> c_17() }
Weak Trs:
  { nats() -> adx(zeros())
  , adx(X) -> n__adx(X)
  , adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y))))
  , zeros() -> cons(n__0(), n__zeros())
  , zeros() -> n__zeros()
  , incr(X) -> n__incr(X)
  , incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__zeros()) -> zeros()
  , activate(n__s(X)) -> s(X)
  , activate(n__incr(X)) -> incr(activate(X))
  , activate(n__adx(X)) -> adx(activate(X))
  , hd(cons(X, Y)) -> activate(X)
  , tl(cons(X, Y)) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: nats^#() -> c_1(adx^#(zeros()), zeros^#())
    , 2: adx^#(cons(X, Y)) ->
         c_3(incr^#(cons(activate(X), n__adx(activate(Y)))),
             activate^#(X),
             activate^#(Y))
    , 3: incr^#(cons(X, Y)) -> c_7(activate^#(X), activate^#(Y))
    , 4: activate^#(n__0()) -> c_9(0^#())
    , 5: activate^#(n__zeros()) -> c_10(zeros^#())
    , 6: activate^#(n__s(X)) -> c_11(s^#(X))
    , 7: activate^#(n__incr(X)) ->
         c_12(incr^#(activate(X)), activate^#(X))
    , 8: activate^#(n__adx(X)) ->
         c_13(adx^#(activate(X)), activate^#(X))
    , 9: hd^#(cons(X, Y)) -> c_14(activate^#(X))
    , 10: tl^#(cons(X, Y)) -> c_15(activate^#(Y))
    , 11: adx^#(X) -> c_2()
    , 12: zeros^#() -> c_4()
    , 13: zeros^#() -> c_5()
    , 14: incr^#(X) -> c_6()
    , 15: activate^#(X) -> c_8()
    , 16: 0^#() -> c_16()
    , 17: s^#(X) -> c_17() }

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_3(incr^#(cons(activate(X), n__adx(activate(Y)))),
        activate^#(X),
        activate^#(Y))
  , incr^#(cons(X, Y)) -> c_7(activate^#(X), activate^#(Y))
  , activate^#(n__incr(X)) ->
    c_12(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_13(adx^#(activate(X)), activate^#(X))
  , hd^#(cons(X, Y)) -> c_14(activate^#(X))
  , tl^#(cons(X, Y)) -> c_15(activate^#(Y)) }
Weak DPs:
  { adx^#(X) -> c_2()
  , zeros^#() -> c_4()
  , zeros^#() -> c_5()
  , incr^#(X) -> c_6()
  , activate^#(X) -> c_8()
  , activate^#(n__0()) -> c_9(0^#())
  , activate^#(n__zeros()) -> c_10(zeros^#())
  , activate^#(n__s(X)) -> c_11(s^#(X))
  , 0^#() -> c_16()
  , s^#(X) -> c_17() }
Weak Trs:
  { nats() -> adx(zeros())
  , adx(X) -> n__adx(X)
  , adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y))))
  , zeros() -> cons(n__0(), n__zeros())
  , zeros() -> n__zeros()
  , incr(X) -> n__incr(X)
  , incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__zeros()) -> zeros()
  , activate(n__s(X)) -> s(X)
  , activate(n__incr(X)) -> incr(activate(X))
  , activate(n__adx(X)) -> adx(activate(X))
  , hd(cons(X, Y)) -> activate(X)
  , tl(cons(X, Y)) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X) }
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.

{ adx^#(X) -> c_2()
, zeros^#() -> c_4()
, zeros^#() -> c_5()
, incr^#(X) -> c_6()
, activate^#(X) -> c_8()
, activate^#(n__0()) -> c_9(0^#())
, activate^#(n__zeros()) -> c_10(zeros^#())
, activate^#(n__s(X)) -> c_11(s^#(X))
, 0^#() -> c_16()
, s^#(X) -> c_17() }

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_3(incr^#(cons(activate(X), n__adx(activate(Y)))),
        activate^#(X),
        activate^#(Y))
  , incr^#(cons(X, Y)) -> c_7(activate^#(X), activate^#(Y))
  , activate^#(n__incr(X)) ->
    c_12(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_13(adx^#(activate(X)), activate^#(X))
  , hd^#(cons(X, Y)) -> c_14(activate^#(X))
  , tl^#(cons(X, Y)) -> c_15(activate^#(Y)) }
Weak Trs:
  { nats() -> adx(zeros())
  , adx(X) -> n__adx(X)
  , adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y))))
  , zeros() -> cons(n__0(), n__zeros())
  , zeros() -> n__zeros()
  , incr(X) -> n__incr(X)
  , incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__zeros()) -> zeros()
  , activate(n__s(X)) -> s(X)
  , activate(n__incr(X)) -> incr(activate(X))
  , activate(n__adx(X)) -> adx(activate(X))
  , hd(cons(X, Y)) -> activate(X)
  , tl(cons(X, Y)) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { nats^#() -> c_1(adx^#(zeros()), zeros^#()) }

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

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

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { adx(X) -> n__adx(X)
    , adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y))))
    , zeros() -> cons(n__0(), n__zeros())
    , zeros() -> n__zeros()
    , incr(X) -> n__incr(X)
    , incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y)))
    , activate(X) -> X
    , activate(n__0()) -> 0()
    , activate(n__zeros()) -> zeros()
    , activate(n__s(X)) -> s(X)
    , activate(n__incr(X)) -> incr(activate(X))
    , activate(n__adx(X)) -> adx(activate(X))
    , 0() -> n__0()
    , s(X) -> n__s(X) }

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

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

Consider the dependency graph

  1: nats^#() -> c_1(adx^#(zeros()))
     -->_1 adx^#(cons(X, Y)) ->
           c_2(incr^#(cons(activate(X), n__adx(activate(Y)))),
               activate^#(X),
               activate^#(Y)) :2
  
  2: adx^#(cons(X, Y)) ->
     c_2(incr^#(cons(activate(X), n__adx(activate(Y)))),
         activate^#(X),
         activate^#(Y))
     -->_3 activate^#(n__adx(X)) ->
           c_5(adx^#(activate(X)), activate^#(X)) :5
     -->_2 activate^#(n__adx(X)) ->
           c_5(adx^#(activate(X)), activate^#(X)) :5
     -->_3 activate^#(n__incr(X)) ->
           c_4(incr^#(activate(X)), activate^#(X)) :4
     -->_2 activate^#(n__incr(X)) ->
           c_4(incr^#(activate(X)), activate^#(X)) :4
     -->_1 incr^#(cons(X, Y)) -> c_3(activate^#(X), activate^#(Y)) :3
  
  3: incr^#(cons(X, Y)) -> c_3(activate^#(X), activate^#(Y))
     -->_2 activate^#(n__adx(X)) ->
           c_5(adx^#(activate(X)), activate^#(X)) :5
     -->_1 activate^#(n__adx(X)) ->
           c_5(adx^#(activate(X)), activate^#(X)) :5
     -->_2 activate^#(n__incr(X)) ->
           c_4(incr^#(activate(X)), activate^#(X)) :4
     -->_1 activate^#(n__incr(X)) ->
           c_4(incr^#(activate(X)), activate^#(X)) :4
  
  4: activate^#(n__incr(X)) ->
     c_4(incr^#(activate(X)), activate^#(X))
     -->_2 activate^#(n__adx(X)) ->
           c_5(adx^#(activate(X)), activate^#(X)) :5
     -->_2 activate^#(n__incr(X)) ->
           c_4(incr^#(activate(X)), activate^#(X)) :4
     -->_1 incr^#(cons(X, Y)) -> c_3(activate^#(X), activate^#(Y)) :3
  
  5: activate^#(n__adx(X)) -> c_5(adx^#(activate(X)), activate^#(X))
     -->_2 activate^#(n__adx(X)) ->
           c_5(adx^#(activate(X)), activate^#(X)) :5
     -->_2 activate^#(n__incr(X)) ->
           c_4(incr^#(activate(X)), activate^#(X)) :4
     -->_1 adx^#(cons(X, Y)) ->
           c_2(incr^#(cons(activate(X), n__adx(activate(Y)))),
               activate^#(X),
               activate^#(Y)) :2
  
  6: hd^#(cons(X, Y)) -> c_6(activate^#(X))
     -->_1 activate^#(n__adx(X)) ->
           c_5(adx^#(activate(X)), activate^#(X)) :5
     -->_1 activate^#(n__incr(X)) ->
           c_4(incr^#(activate(X)), activate^#(X)) :4
  
  7: tl^#(cons(X, Y)) -> c_7(activate^#(Y))
     -->_1 activate^#(n__adx(X)) ->
           c_5(adx^#(activate(X)), activate^#(X)) :5
     -->_1 activate^#(n__incr(X)) ->
           c_4(incr^#(activate(X)), activate^#(X)) :4
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

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


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

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

The input cannot be shown compatible

Arrrr..