MAYBE

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

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

We add following dependency tuples:

Strict DPs:
  { incr^#(X) -> c_1()
  , incr^#(nil()) -> c_2()
  , incr^#(cons(X, L)) -> c_3(activate^#(L))
  , activate^#(X) -> c_4()
  , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X))
  , activate^#(n__zeros()) -> c_7(zeros^#())
  , adx^#(X) -> c_8()
  , adx^#(nil()) -> c_9()
  , adx^#(cons(X, L)) ->
    c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L))
  , zeros^#() -> c_12()
  , zeros^#() -> c_13()
  , nats^#() -> c_11(adx^#(zeros()), zeros^#())
  , head^#(cons(X, L)) -> c_14()
  , tail^#(cons(X, L)) -> c_15(activate^#(L)) }

and mark the set of starting terms.

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

Strict DPs:
  { incr^#(X) -> c_1()
  , incr^#(nil()) -> c_2()
  , incr^#(cons(X, L)) -> c_3(activate^#(L))
  , activate^#(X) -> c_4()
  , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X))
  , activate^#(n__zeros()) -> c_7(zeros^#())
  , adx^#(X) -> c_8()
  , adx^#(nil()) -> c_9()
  , adx^#(cons(X, L)) ->
    c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L))
  , zeros^#() -> c_12()
  , zeros^#() -> c_13()
  , nats^#() -> c_11(adx^#(zeros()), zeros^#())
  , head^#(cons(X, L)) -> c_14()
  , tail^#(cons(X, L)) -> c_15(activate^#(L)) }
Weak Trs:
  { incr(X) -> n__incr(X)
  , incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L)))
  , activate(X) -> X
  , activate(n__incr(X)) -> incr(activate(X))
  , activate(n__adx(X)) -> adx(activate(X))
  , activate(n__zeros()) -> zeros()
  , adx(X) -> n__adx(X)
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L))))
  , nats() -> adx(zeros())
  , zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , head(cons(X, L)) -> X
  , tail(cons(X, L)) -> activate(L) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: incr^#(X) -> c_1()
    , 2: incr^#(nil()) -> c_2()
    , 3: incr^#(cons(X, L)) -> c_3(activate^#(L))
    , 4: activate^#(X) -> c_4()
    , 5: activate^#(n__incr(X)) ->
         c_5(incr^#(activate(X)), activate^#(X))
    , 6: activate^#(n__adx(X)) ->
         c_6(adx^#(activate(X)), activate^#(X))
    , 7: activate^#(n__zeros()) -> c_7(zeros^#())
    , 8: adx^#(X) -> c_8()
    , 9: adx^#(nil()) -> c_9()
    , 10: adx^#(cons(X, L)) ->
          c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L))
    , 11: zeros^#() -> c_12()
    , 12: zeros^#() -> c_13()
    , 13: nats^#() -> c_11(adx^#(zeros()), zeros^#())
    , 14: head^#(cons(X, L)) -> c_14()
    , 15: tail^#(cons(X, L)) -> c_15(activate^#(L)) }

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

Strict DPs:
  { incr^#(cons(X, L)) -> c_3(activate^#(L))
  , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X))
  , activate^#(n__zeros()) -> c_7(zeros^#())
  , adx^#(cons(X, L)) ->
    c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L))
  , nats^#() -> c_11(adx^#(zeros()), zeros^#())
  , tail^#(cons(X, L)) -> c_15(activate^#(L)) }
Weak DPs:
  { incr^#(X) -> c_1()
  , incr^#(nil()) -> c_2()
  , activate^#(X) -> c_4()
  , adx^#(X) -> c_8()
  , adx^#(nil()) -> c_9()
  , zeros^#() -> c_12()
  , zeros^#() -> c_13()
  , head^#(cons(X, L)) -> c_14() }
Weak Trs:
  { incr(X) -> n__incr(X)
  , incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L)))
  , activate(X) -> X
  , activate(n__incr(X)) -> incr(activate(X))
  , activate(n__adx(X)) -> adx(activate(X))
  , activate(n__zeros()) -> zeros()
  , adx(X) -> n__adx(X)
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L))))
  , nats() -> adx(zeros())
  , zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , head(cons(X, L)) -> X
  , tail(cons(X, L)) -> activate(L) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: incr^#(cons(X, L)) -> c_3(activate^#(L))
    , 2: activate^#(n__incr(X)) ->
         c_5(incr^#(activate(X)), activate^#(X))
    , 3: activate^#(n__adx(X)) ->
         c_6(adx^#(activate(X)), activate^#(X))
    , 4: activate^#(n__zeros()) -> c_7(zeros^#())
    , 5: adx^#(cons(X, L)) ->
         c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L))
    , 6: nats^#() -> c_11(adx^#(zeros()), zeros^#())
    , 7: tail^#(cons(X, L)) -> c_15(activate^#(L))
    , 8: incr^#(X) -> c_1()
    , 9: incr^#(nil()) -> c_2()
    , 10: activate^#(X) -> c_4()
    , 11: adx^#(X) -> c_8()
    , 12: adx^#(nil()) -> c_9()
    , 13: zeros^#() -> c_12()
    , 14: zeros^#() -> c_13()
    , 15: head^#(cons(X, L)) -> c_14() }

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

Strict DPs:
  { incr^#(cons(X, L)) -> c_3(activate^#(L))
  , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X))
  , adx^#(cons(X, L)) ->
    c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L))
  , nats^#() -> c_11(adx^#(zeros()), zeros^#())
  , tail^#(cons(X, L)) -> c_15(activate^#(L)) }
Weak DPs:
  { incr^#(X) -> c_1()
  , incr^#(nil()) -> c_2()
  , activate^#(X) -> c_4()
  , activate^#(n__zeros()) -> c_7(zeros^#())
  , adx^#(X) -> c_8()
  , adx^#(nil()) -> c_9()
  , zeros^#() -> c_12()
  , zeros^#() -> c_13()
  , head^#(cons(X, L)) -> c_14() }
Weak Trs:
  { incr(X) -> n__incr(X)
  , incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L)))
  , activate(X) -> X
  , activate(n__incr(X)) -> incr(activate(X))
  , activate(n__adx(X)) -> adx(activate(X))
  , activate(n__zeros()) -> zeros()
  , adx(X) -> n__adx(X)
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L))))
  , nats() -> adx(zeros())
  , zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , head(cons(X, L)) -> X
  , tail(cons(X, L)) -> activate(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^#(X) -> c_1()
, incr^#(nil()) -> c_2()
, activate^#(X) -> c_4()
, activate^#(n__zeros()) -> c_7(zeros^#())
, adx^#(X) -> c_8()
, adx^#(nil()) -> c_9()
, zeros^#() -> c_12()
, zeros^#() -> c_13()
, head^#(cons(X, L)) -> c_14() }

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

Strict DPs:
  { incr^#(cons(X, L)) -> c_3(activate^#(L))
  , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X))
  , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X))
  , adx^#(cons(X, L)) ->
    c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L))
  , nats^#() -> c_11(adx^#(zeros()), zeros^#())
  , tail^#(cons(X, L)) -> c_15(activate^#(L)) }
Weak Trs:
  { incr(X) -> n__incr(X)
  , incr(nil()) -> nil()
  , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L)))
  , activate(X) -> X
  , activate(n__incr(X)) -> incr(activate(X))
  , activate(n__adx(X)) -> adx(activate(X))
  , activate(n__zeros()) -> zeros()
  , adx(X) -> n__adx(X)
  , adx(nil()) -> nil()
  , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L))))
  , nats() -> adx(zeros())
  , zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , head(cons(X, L)) -> X
  , tail(cons(X, L)) -> activate(L) }
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_11(adx^#(zeros()), zeros^#()) }

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

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

We replace rewrite rules by usable rules:

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

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

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

Consider the dependency graph

  1: incr^#(cons(X, L)) -> c_1(activate^#(L))
     -->_1 activate^#(n__adx(X)) ->
           c_3(adx^#(activate(X)), activate^#(X)) :3
     -->_1 activate^#(n__incr(X)) ->
           c_2(incr^#(activate(X)), activate^#(X)) :2
  
  2: activate^#(n__incr(X)) ->
     c_2(incr^#(activate(X)), activate^#(X))
     -->_2 activate^#(n__adx(X)) ->
           c_3(adx^#(activate(X)), activate^#(X)) :3
     -->_2 activate^#(n__incr(X)) ->
           c_2(incr^#(activate(X)), activate^#(X)) :2
     -->_1 incr^#(cons(X, L)) -> c_1(activate^#(L)) :1
  
  3: activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X))
     -->_1 adx^#(cons(X, L)) ->
           c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) :4
     -->_2 activate^#(n__adx(X)) ->
           c_3(adx^#(activate(X)), activate^#(X)) :3
     -->_2 activate^#(n__incr(X)) ->
           c_2(incr^#(activate(X)), activate^#(X)) :2
  
  4: adx^#(cons(X, L)) ->
     c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L))
     -->_2 activate^#(n__adx(X)) ->
           c_3(adx^#(activate(X)), activate^#(X)) :3
     -->_2 activate^#(n__incr(X)) ->
           c_2(incr^#(activate(X)), activate^#(X)) :2
     -->_1 incr^#(cons(X, L)) -> c_1(activate^#(L)) :1
  
  5: nats^#() -> c_5(adx^#(zeros()))
     -->_1 adx^#(cons(X, L)) ->
           c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) :4
  
  6: tail^#(cons(X, L)) -> c_6(activate^#(L))
     -->_1 activate^#(n__adx(X)) ->
           c_3(adx^#(activate(X)), activate^#(X)) :3
     -->_1 activate^#(n__incr(X)) ->
           c_2(incr^#(activate(X)), activate^#(X)) :2
  

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

  { tail^#(cons(X, L)) -> c_6(activate^#(L)) }


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

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

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..