MAYBE

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

Strict Trs:
  { from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , s(X) -> n__s(X)
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(n__s(X))))
  , from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , length^#(n__cons(X, Y)) ->
    c_5(s^#(length1(activate(Y))),
        length1^#(activate(Y)),
        activate^#(Y))
  , s^#(X) -> c_6()
  , length1^#(X) -> c_7(length^#(activate(X)), activate^#(X))
  , activate^#(X) -> c_8()
  , activate^#(n__from(X)) -> c_9(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
  , activate^#(n__nil()) -> c_11(nil^#())
  , activate^#(n__cons(X1, X2)) ->
    c_12(cons^#(activate(X1), X2), activate^#(X1))
  , nil^#() -> c_13() }

and mark the set of starting terms.

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

Strict DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(n__s(X))))
  , from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , length^#(n__cons(X, Y)) ->
    c_5(s^#(length1(activate(Y))),
        length1^#(activate(Y)),
        activate^#(Y))
  , s^#(X) -> c_6()
  , length1^#(X) -> c_7(length^#(activate(X)), activate^#(X))
  , activate^#(X) -> c_8()
  , activate^#(n__from(X)) -> c_9(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
  , activate^#(n__nil()) -> c_11(nil^#())
  , activate^#(n__cons(X1, X2)) ->
    c_12(cons^#(activate(X1), X2), activate^#(X1))
  , nil^#() -> c_13() }
Weak Trs:
  { from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , s(X) -> n__s(X)
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: from^#(X) -> c_1(cons^#(X, n__from(n__s(X))))
    , 2: from^#(X) -> c_2()
    , 3: cons^#(X1, X2) -> c_3()
    , 4: length^#(n__nil()) -> c_4()
    , 5: length^#(n__cons(X, Y)) ->
         c_5(s^#(length1(activate(Y))),
             length1^#(activate(Y)),
             activate^#(Y))
    , 6: s^#(X) -> c_6()
    , 7: length1^#(X) -> c_7(length^#(activate(X)), activate^#(X))
    , 8: activate^#(X) -> c_8()
    , 9: activate^#(n__from(X)) ->
         c_9(from^#(activate(X)), activate^#(X))
    , 10: activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
    , 11: activate^#(n__nil()) -> c_11(nil^#())
    , 12: activate^#(n__cons(X1, X2)) ->
          c_12(cons^#(activate(X1), X2), activate^#(X1))
    , 13: nil^#() -> c_13() }

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

Strict DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(n__s(X))))
  , length^#(n__cons(X, Y)) ->
    c_5(s^#(length1(activate(Y))),
        length1^#(activate(Y)),
        activate^#(Y))
  , length1^#(X) -> c_7(length^#(activate(X)), activate^#(X))
  , activate^#(n__from(X)) -> c_9(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
  , activate^#(n__nil()) -> c_11(nil^#())
  , activate^#(n__cons(X1, X2)) ->
    c_12(cons^#(activate(X1), X2), activate^#(X1)) }
Weak DPs:
  { from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , s^#(X) -> c_6()
  , activate^#(X) -> c_8()
  , nil^#() -> c_13() }
Weak Trs:
  { from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , s(X) -> n__s(X)
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: from^#(X) -> c_1(cons^#(X, n__from(n__s(X))))
    , 2: length^#(n__cons(X, Y)) ->
         c_5(s^#(length1(activate(Y))),
             length1^#(activate(Y)),
             activate^#(Y))
    , 3: length1^#(X) -> c_7(length^#(activate(X)), activate^#(X))
    , 4: activate^#(n__from(X)) ->
         c_9(from^#(activate(X)), activate^#(X))
    , 5: activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
    , 6: activate^#(n__nil()) -> c_11(nil^#())
    , 7: activate^#(n__cons(X1, X2)) ->
         c_12(cons^#(activate(X1), X2), activate^#(X1))
    , 8: from^#(X) -> c_2()
    , 9: cons^#(X1, X2) -> c_3()
    , 10: length^#(n__nil()) -> c_4()
    , 11: s^#(X) -> c_6()
    , 12: activate^#(X) -> c_8()
    , 13: nil^#() -> c_13() }

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

Strict DPs:
  { length^#(n__cons(X, Y)) ->
    c_5(s^#(length1(activate(Y))),
        length1^#(activate(Y)),
        activate^#(Y))
  , length1^#(X) -> c_7(length^#(activate(X)), activate^#(X))
  , activate^#(n__from(X)) -> c_9(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
  , activate^#(n__cons(X1, X2)) ->
    c_12(cons^#(activate(X1), X2), activate^#(X1)) }
Weak DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(n__s(X))))
  , from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , s^#(X) -> c_6()
  , activate^#(X) -> c_8()
  , activate^#(n__nil()) -> c_11(nil^#())
  , nil^#() -> c_13() }
Weak Trs:
  { from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , s(X) -> n__s(X)
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , nil() -> n__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.

{ from^#(X) -> c_1(cons^#(X, n__from(n__s(X))))
, from^#(X) -> c_2()
, cons^#(X1, X2) -> c_3()
, length^#(n__nil()) -> c_4()
, s^#(X) -> c_6()
, activate^#(X) -> c_8()
, activate^#(n__nil()) -> c_11(nil^#())
, nil^#() -> c_13() }

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

Strict DPs:
  { length^#(n__cons(X, Y)) ->
    c_5(s^#(length1(activate(Y))),
        length1^#(activate(Y)),
        activate^#(Y))
  , length1^#(X) -> c_7(length^#(activate(X)), activate^#(X))
  , activate^#(n__from(X)) -> c_9(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
  , activate^#(n__cons(X1, X2)) ->
    c_12(cons^#(activate(X1), X2), activate^#(X1)) }
Weak Trs:
  { from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , s(X) -> n__s(X)
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { length^#(n__cons(X, Y)) ->
    c_5(s^#(length1(activate(Y))),
        length1^#(activate(Y)),
        activate^#(Y))
  , activate^#(n__from(X)) -> c_9(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
  , activate^#(n__cons(X1, X2)) ->
    c_12(cons^#(activate(X1), X2), activate^#(X1)) }

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

Strict DPs:
  { length^#(n__cons(X, Y)) ->
    c_1(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_2(length^#(activate(X)), activate^#(X))
  , activate^#(n__from(X)) -> c_3(activate^#(X))
  , activate^#(n__s(X)) -> c_4(activate^#(X))
  , activate^#(n__cons(X1, X2)) -> c_5(activate^#(X1)) }
Weak Trs:
  { from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , s(X) -> n__s(X)
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { from(X) -> cons(X, n__from(n__s(X)))
    , from(X) -> n__from(X)
    , cons(X1, X2) -> n__cons(X1, X2)
    , s(X) -> n__s(X)
    , activate(X) -> X
    , activate(n__from(X)) -> from(activate(X))
    , activate(n__s(X)) -> s(activate(X))
    , activate(n__nil()) -> nil()
    , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
    , nil() -> n__nil() }

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

Strict DPs:
  { length^#(n__cons(X, Y)) ->
    c_1(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_2(length^#(activate(X)), activate^#(X))
  , activate^#(n__from(X)) -> c_3(activate^#(X))
  , activate^#(n__s(X)) -> c_4(activate^#(X))
  , activate^#(n__cons(X1, X2)) -> c_5(activate^#(X1)) }
Weak Trs:
  { from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , s(X) -> n__s(X)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..