MAYBE

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

Strict Trs:
  { a__zeros() -> cons(0(), zeros())
  , a__zeros() -> zeros()
  , a__and(X1, X2) -> and(X1, X2)
  , a__and(tt(), X) -> mark(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(zeros()) -> a__zeros()
  , mark(tt()) -> tt()
  , mark(nil()) -> nil()
  , mark(s(X)) -> s(mark(X))
  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
  , mark(length(X)) -> a__length(mark(X))
  , a__length(X) -> length(X)
  , a__length(cons(N, L)) -> s(a__length(mark(L)))
  , a__length(nil()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { a__zeros^#() -> c_1()
  , a__zeros^#() -> c_2()
  , a__and^#(X1, X2) -> c_3()
  , a__and^#(tt(), X) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(0()) -> c_6()
  , mark^#(zeros()) -> c_7(a__zeros^#())
  , mark^#(tt()) -> c_8()
  , mark^#(nil()) -> c_9()
  , mark^#(s(X)) -> c_10(mark^#(X))
  , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), X2), mark^#(X1))
  , mark^#(length(X)) -> c_12(a__length^#(mark(X)), mark^#(X))
  , a__length^#(X) -> c_13()
  , a__length^#(cons(N, L)) -> c_14(a__length^#(mark(L)), mark^#(L))
  , a__length^#(nil()) -> c_15() }

and mark the set of starting terms.

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

Strict DPs:
  { a__zeros^#() -> c_1()
  , a__zeros^#() -> c_2()
  , a__and^#(X1, X2) -> c_3()
  , a__and^#(tt(), X) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(0()) -> c_6()
  , mark^#(zeros()) -> c_7(a__zeros^#())
  , mark^#(tt()) -> c_8()
  , mark^#(nil()) -> c_9()
  , mark^#(s(X)) -> c_10(mark^#(X))
  , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), X2), mark^#(X1))
  , mark^#(length(X)) -> c_12(a__length^#(mark(X)), mark^#(X))
  , a__length^#(X) -> c_13()
  , a__length^#(cons(N, L)) -> c_14(a__length^#(mark(L)), mark^#(L))
  , a__length^#(nil()) -> c_15() }
Weak Trs:
  { a__zeros() -> cons(0(), zeros())
  , a__zeros() -> zeros()
  , a__and(X1, X2) -> and(X1, X2)
  , a__and(tt(), X) -> mark(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(zeros()) -> a__zeros()
  , mark(tt()) -> tt()
  , mark(nil()) -> nil()
  , mark(s(X)) -> s(mark(X))
  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
  , mark(length(X)) -> a__length(mark(X))
  , a__length(X) -> length(X)
  , a__length(cons(N, L)) -> s(a__length(mark(L)))
  , a__length(nil()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: a__zeros^#() -> c_1()
    , 2: a__zeros^#() -> c_2()
    , 3: a__and^#(X1, X2) -> c_3()
    , 4: a__and^#(tt(), X) -> c_4(mark^#(X))
    , 5: mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
    , 6: mark^#(0()) -> c_6()
    , 7: mark^#(zeros()) -> c_7(a__zeros^#())
    , 8: mark^#(tt()) -> c_8()
    , 9: mark^#(nil()) -> c_9()
    , 10: mark^#(s(X)) -> c_10(mark^#(X))
    , 11: mark^#(and(X1, X2)) ->
          c_11(a__and^#(mark(X1), X2), mark^#(X1))
    , 12: mark^#(length(X)) -> c_12(a__length^#(mark(X)), mark^#(X))
    , 13: a__length^#(X) -> c_13()
    , 14: a__length^#(cons(N, L)) ->
          c_14(a__length^#(mark(L)), mark^#(L))
    , 15: a__length^#(nil()) -> c_15() }

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

Strict DPs:
  { a__and^#(tt(), X) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(zeros()) -> c_7(a__zeros^#())
  , mark^#(s(X)) -> c_10(mark^#(X))
  , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), X2), mark^#(X1))
  , mark^#(length(X)) -> c_12(a__length^#(mark(X)), mark^#(X))
  , a__length^#(cons(N, L)) ->
    c_14(a__length^#(mark(L)), mark^#(L)) }
Weak DPs:
  { a__zeros^#() -> c_1()
  , a__zeros^#() -> c_2()
  , a__and^#(X1, X2) -> c_3()
  , mark^#(0()) -> c_6()
  , mark^#(tt()) -> c_8()
  , mark^#(nil()) -> c_9()
  , a__length^#(X) -> c_13()
  , a__length^#(nil()) -> c_15() }
Weak Trs:
  { a__zeros() -> cons(0(), zeros())
  , a__zeros() -> zeros()
  , a__and(X1, X2) -> and(X1, X2)
  , a__and(tt(), X) -> mark(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(zeros()) -> a__zeros()
  , mark(tt()) -> tt()
  , mark(nil()) -> nil()
  , mark(s(X)) -> s(mark(X))
  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
  , mark(length(X)) -> a__length(mark(X))
  , a__length(X) -> length(X)
  , a__length(cons(N, L)) -> s(a__length(mark(L)))
  , a__length(nil()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: a__and^#(tt(), X) -> c_4(mark^#(X))
    , 2: mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
    , 3: mark^#(zeros()) -> c_7(a__zeros^#())
    , 4: mark^#(s(X)) -> c_10(mark^#(X))
    , 5: mark^#(and(X1, X2)) ->
         c_11(a__and^#(mark(X1), X2), mark^#(X1))
    , 6: mark^#(length(X)) -> c_12(a__length^#(mark(X)), mark^#(X))
    , 7: a__length^#(cons(N, L)) ->
         c_14(a__length^#(mark(L)), mark^#(L))
    , 8: a__zeros^#() -> c_1()
    , 9: a__zeros^#() -> c_2()
    , 10: a__and^#(X1, X2) -> c_3()
    , 11: mark^#(0()) -> c_6()
    , 12: mark^#(tt()) -> c_8()
    , 13: mark^#(nil()) -> c_9()
    , 14: a__length^#(X) -> c_13()
    , 15: a__length^#(nil()) -> c_15() }

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

Strict DPs:
  { a__and^#(tt(), X) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(s(X)) -> c_10(mark^#(X))
  , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), X2), mark^#(X1))
  , mark^#(length(X)) -> c_12(a__length^#(mark(X)), mark^#(X))
  , a__length^#(cons(N, L)) ->
    c_14(a__length^#(mark(L)), mark^#(L)) }
Weak DPs:
  { a__zeros^#() -> c_1()
  , a__zeros^#() -> c_2()
  , a__and^#(X1, X2) -> c_3()
  , mark^#(0()) -> c_6()
  , mark^#(zeros()) -> c_7(a__zeros^#())
  , mark^#(tt()) -> c_8()
  , mark^#(nil()) -> c_9()
  , a__length^#(X) -> c_13()
  , a__length^#(nil()) -> c_15() }
Weak Trs:
  { a__zeros() -> cons(0(), zeros())
  , a__zeros() -> zeros()
  , a__and(X1, X2) -> and(X1, X2)
  , a__and(tt(), X) -> mark(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(zeros()) -> a__zeros()
  , mark(tt()) -> tt()
  , mark(nil()) -> nil()
  , mark(s(X)) -> s(mark(X))
  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
  , mark(length(X)) -> a__length(mark(X))
  , a__length(X) -> length(X)
  , a__length(cons(N, L)) -> s(a__length(mark(L)))
  , a__length(nil()) -> 0() }
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.

{ a__zeros^#() -> c_1()
, a__zeros^#() -> c_2()
, a__and^#(X1, X2) -> c_3()
, mark^#(0()) -> c_6()
, mark^#(zeros()) -> c_7(a__zeros^#())
, mark^#(tt()) -> c_8()
, mark^#(nil()) -> c_9()
, a__length^#(X) -> c_13()
, a__length^#(nil()) -> c_15() }

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

Strict DPs:
  { a__and^#(tt(), X) -> c_4(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_5(mark^#(X1))
  , mark^#(s(X)) -> c_10(mark^#(X))
  , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), X2), mark^#(X1))
  , mark^#(length(X)) -> c_12(a__length^#(mark(X)), mark^#(X))
  , a__length^#(cons(N, L)) ->
    c_14(a__length^#(mark(L)), mark^#(L)) }
Weak Trs:
  { a__zeros() -> cons(0(), zeros())
  , a__zeros() -> zeros()
  , a__and(X1, X2) -> and(X1, X2)
  , a__and(tt(), X) -> mark(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(zeros()) -> a__zeros()
  , mark(tt()) -> tt()
  , mark(nil()) -> nil()
  , mark(s(X)) -> s(mark(X))
  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
  , mark(length(X)) -> a__length(mark(X))
  , a__length(X) -> length(X)
  , a__length(cons(N, L)) -> s(a__length(mark(L)))
  , a__length(nil()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..