YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { a__eq(X, Y) -> false()
  , a__eq(X1, X2) -> eq(X1, X2)
  , a__eq(0(), 0()) -> true()
  , a__eq(s(X), s(Y)) -> a__eq(X, Y)
  , a__inf(X) -> cons(X, inf(s(X)))
  , a__inf(X) -> inf(X)
  , a__take(X1, X2) -> take(X1, X2)
  , a__take(0(), X) -> nil()
  , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
  , a__length(X) -> length(X)
  , a__length(cons(X, L)) -> s(length(L))
  , a__length(nil()) -> 0()
  , mark(0()) -> 0()
  , mark(true()) -> true()
  , mark(s(X)) -> s(X)
  , mark(false()) -> false()
  , mark(cons(X1, X2)) -> cons(X1, X2)
  , mark(inf(X)) -> a__inf(mark(X))
  , mark(nil()) -> nil()
  , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
  , mark(length(X)) -> a__length(mark(X))
  , mark(eq(X1, X2)) -> a__eq(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

We add following dependency tuples:

Strict DPs:
  { a__eq^#(X, Y) -> c_1()
  , a__eq^#(X1, X2) -> c_2()
  , a__eq^#(0(), 0()) -> c_3()
  , a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y))
  , a__inf^#(X) -> c_5()
  , a__inf^#(X) -> c_6()
  , a__take^#(X1, X2) -> c_7()
  , a__take^#(0(), X) -> c_8()
  , a__take^#(s(X), cons(Y, L)) -> c_9()
  , a__length^#(X) -> c_10()
  , a__length^#(cons(X, L)) -> c_11()
  , a__length^#(nil()) -> c_12()
  , mark^#(0()) -> c_13()
  , mark^#(true()) -> c_14()
  , mark^#(s(X)) -> c_15()
  , mark^#(false()) -> c_16()
  , mark^#(cons(X1, X2)) -> c_17()
  , mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X))
  , mark^#(nil()) -> c_19()
  , mark^#(take(X1, X2)) ->
    c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X))
  , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { a__eq^#(X, Y) -> c_1()
  , a__eq^#(X1, X2) -> c_2()
  , a__eq^#(0(), 0()) -> c_3()
  , a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y))
  , a__inf^#(X) -> c_5()
  , a__inf^#(X) -> c_6()
  , a__take^#(X1, X2) -> c_7()
  , a__take^#(0(), X) -> c_8()
  , a__take^#(s(X), cons(Y, L)) -> c_9()
  , a__length^#(X) -> c_10()
  , a__length^#(cons(X, L)) -> c_11()
  , a__length^#(nil()) -> c_12()
  , mark^#(0()) -> c_13()
  , mark^#(true()) -> c_14()
  , mark^#(s(X)) -> c_15()
  , mark^#(false()) -> c_16()
  , mark^#(cons(X1, X2)) -> c_17()
  , mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X))
  , mark^#(nil()) -> c_19()
  , mark^#(take(X1, X2)) ->
    c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X))
  , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) }
Weak Trs:
  { a__eq(X, Y) -> false()
  , a__eq(X1, X2) -> eq(X1, X2)
  , a__eq(0(), 0()) -> true()
  , a__eq(s(X), s(Y)) -> a__eq(X, Y)
  , a__inf(X) -> cons(X, inf(s(X)))
  , a__inf(X) -> inf(X)
  , a__take(X1, X2) -> take(X1, X2)
  , a__take(0(), X) -> nil()
  , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
  , a__length(X) -> length(X)
  , a__length(cons(X, L)) -> s(length(L))
  , a__length(nil()) -> 0()
  , mark(0()) -> 0()
  , mark(true()) -> true()
  , mark(s(X)) -> s(X)
  , mark(false()) -> false()
  , mark(cons(X1, X2)) -> cons(X1, X2)
  , mark(inf(X)) -> a__inf(mark(X))
  , mark(nil()) -> nil()
  , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
  , mark(length(X)) -> a__length(mark(X))
  , mark(eq(X1, X2)) -> a__eq(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

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

  DPs:
    { 1: a__eq^#(X, Y) -> c_1()
    , 2: a__eq^#(X1, X2) -> c_2()
    , 3: a__eq^#(0(), 0()) -> c_3()
    , 4: a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y))
    , 5: a__inf^#(X) -> c_5()
    , 6: a__inf^#(X) -> c_6()
    , 7: a__take^#(X1, X2) -> c_7()
    , 8: a__take^#(0(), X) -> c_8()
    , 9: a__take^#(s(X), cons(Y, L)) -> c_9()
    , 10: a__length^#(X) -> c_10()
    , 11: a__length^#(cons(X, L)) -> c_11()
    , 12: a__length^#(nil()) -> c_12()
    , 13: mark^#(0()) -> c_13()
    , 14: mark^#(true()) -> c_14()
    , 15: mark^#(s(X)) -> c_15()
    , 16: mark^#(false()) -> c_16()
    , 17: mark^#(cons(X1, X2)) -> c_17()
    , 18: mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X))
    , 19: mark^#(nil()) -> c_19()
    , 20: mark^#(take(X1, X2)) ->
          c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 21: mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X))
    , 22: mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y))
  , mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X))
  , mark^#(take(X1, X2)) ->
    c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X))
  , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) }
Weak DPs:
  { a__eq^#(X, Y) -> c_1()
  , a__eq^#(X1, X2) -> c_2()
  , a__eq^#(0(), 0()) -> c_3()
  , a__inf^#(X) -> c_5()
  , a__inf^#(X) -> c_6()
  , a__take^#(X1, X2) -> c_7()
  , a__take^#(0(), X) -> c_8()
  , a__take^#(s(X), cons(Y, L)) -> c_9()
  , a__length^#(X) -> c_10()
  , a__length^#(cons(X, L)) -> c_11()
  , a__length^#(nil()) -> c_12()
  , mark^#(0()) -> c_13()
  , mark^#(true()) -> c_14()
  , mark^#(s(X)) -> c_15()
  , mark^#(false()) -> c_16()
  , mark^#(cons(X1, X2)) -> c_17()
  , mark^#(nil()) -> c_19() }
Weak Trs:
  { a__eq(X, Y) -> false()
  , a__eq(X1, X2) -> eq(X1, X2)
  , a__eq(0(), 0()) -> true()
  , a__eq(s(X), s(Y)) -> a__eq(X, Y)
  , a__inf(X) -> cons(X, inf(s(X)))
  , a__inf(X) -> inf(X)
  , a__take(X1, X2) -> take(X1, X2)
  , a__take(0(), X) -> nil()
  , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
  , a__length(X) -> length(X)
  , a__length(cons(X, L)) -> s(length(L))
  , a__length(nil()) -> 0()
  , mark(0()) -> 0()
  , mark(true()) -> true()
  , mark(s(X)) -> s(X)
  , mark(false()) -> false()
  , mark(cons(X1, X2)) -> cons(X1, X2)
  , mark(inf(X)) -> a__inf(mark(X))
  , mark(nil()) -> nil()
  , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
  , mark(length(X)) -> a__length(mark(X))
  , mark(eq(X1, X2)) -> a__eq(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ a__eq^#(X, Y) -> c_1()
, a__eq^#(X1, X2) -> c_2()
, a__eq^#(0(), 0()) -> c_3()
, a__inf^#(X) -> c_5()
, a__inf^#(X) -> c_6()
, a__take^#(X1, X2) -> c_7()
, a__take^#(0(), X) -> c_8()
, a__take^#(s(X), cons(Y, L)) -> c_9()
, a__length^#(X) -> c_10()
, a__length^#(cons(X, L)) -> c_11()
, a__length^#(nil()) -> c_12()
, mark^#(0()) -> c_13()
, mark^#(true()) -> c_14()
, mark^#(s(X)) -> c_15()
, mark^#(false()) -> c_16()
, mark^#(cons(X1, X2)) -> c_17()
, mark^#(nil()) -> c_19() }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y))
  , mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X))
  , mark^#(take(X1, X2)) ->
    c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X))
  , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) }
Weak Trs:
  { a__eq(X, Y) -> false()
  , a__eq(X1, X2) -> eq(X1, X2)
  , a__eq(0(), 0()) -> true()
  , a__eq(s(X), s(Y)) -> a__eq(X, Y)
  , a__inf(X) -> cons(X, inf(s(X)))
  , a__inf(X) -> inf(X)
  , a__take(X1, X2) -> take(X1, X2)
  , a__take(0(), X) -> nil()
  , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
  , a__length(X) -> length(X)
  , a__length(cons(X, L)) -> s(length(L))
  , a__length(nil()) -> 0()
  , mark(0()) -> 0()
  , mark(true()) -> true()
  , mark(s(X)) -> s(X)
  , mark(false()) -> false()
  , mark(cons(X1, X2)) -> cons(X1, X2)
  , mark(inf(X)) -> a__inf(mark(X))
  , mark(nil()) -> nil()
  , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
  , mark(length(X)) -> a__length(mark(X))
  , mark(eq(X1, X2)) -> a__eq(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

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

  { mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X))
  , mark^#(take(X1, X2)) ->
    c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X)) }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { a__eq^#(s(X), s(Y)) -> c_1(a__eq^#(X, Y))
  , mark^#(inf(X)) -> c_2(mark^#(X))
  , mark^#(take(X1, X2)) -> c_3(mark^#(X1), mark^#(X2))
  , mark^#(length(X)) -> c_4(mark^#(X))
  , mark^#(eq(X1, X2)) -> c_5(a__eq^#(X1, X2)) }
Weak Trs:
  { a__eq(X, Y) -> false()
  , a__eq(X1, X2) -> eq(X1, X2)
  , a__eq(0(), 0()) -> true()
  , a__eq(s(X), s(Y)) -> a__eq(X, Y)
  , a__inf(X) -> cons(X, inf(s(X)))
  , a__inf(X) -> inf(X)
  , a__take(X1, X2) -> take(X1, X2)
  , a__take(0(), X) -> nil()
  , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
  , a__length(X) -> length(X)
  , a__length(cons(X, L)) -> s(length(L))
  , a__length(nil()) -> 0()
  , mark(0()) -> 0()
  , mark(true()) -> true()
  , mark(s(X)) -> s(X)
  , mark(false()) -> false()
  , mark(cons(X1, X2)) -> cons(X1, X2)
  , mark(inf(X)) -> a__inf(mark(X))
  , mark(nil()) -> nil()
  , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
  , mark(length(X)) -> a__length(mark(X))
  , mark(eq(X1, X2)) -> a__eq(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { a__eq^#(s(X), s(Y)) -> c_1(a__eq^#(X, Y))
  , mark^#(inf(X)) -> c_2(mark^#(X))
  , mark^#(take(X1, X2)) -> c_3(mark^#(X1), mark^#(X2))
  , mark^#(length(X)) -> c_4(mark^#(X))
  , mark^#(eq(X1, X2)) -> c_5(a__eq^#(X1, X2)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
  Uargs(c_4) = {1}, Uargs(c_5) = {1}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

            [s](x1) = [1] x1 + [2]         
                                           
          [inf](x1) = [1] x1 + [2]         
                                           
     [take](x1, x2) = [1] x1 + [1] x2 + [2]
                                           
       [length](x1) = [1] x1 + [2]         
                                           
       [eq](x1, x2) = [1] x1 + [1] x2 + [0]
                                           
  [a__eq^#](x1, x2) = [2] x1 + [0]         
                                           
       [mark^#](x1) = [2] x1 + [2]         
                                           
          [c_1](x1) = [1] x1 + [1]         
                                           
          [c_2](x1) = [1] x1 + [0]         
                                           
      [c_3](x1, x2) = [1] x1 + [1] x2 + [1]
                                           
          [c_4](x1) = [1] x1 + [0]         
                                           
          [c_5](x1) = [1] x1 + [1]         

This order satisfies following ordering constraints:

   [a__eq^#(s(X), s(Y))] = [2] X + [4]                  
                         > [2] X + [1]                  
                         = [c_1(a__eq^#(X, Y))]         
                                                        
        [mark^#(inf(X))] = [2] X + [6]                  
                         > [2] X + [2]                  
                         = [c_2(mark^#(X))]             
                                                        
  [mark^#(take(X1, X2))] = [2] X1 + [2] X2 + [6]        
                         > [2] X1 + [2] X2 + [5]        
                         = [c_3(mark^#(X1), mark^#(X2))]
                                                        
     [mark^#(length(X))] = [2] X + [6]                  
                         > [2] X + [2]                  
                         = [c_4(mark^#(X))]             
                                                        
    [mark^#(eq(X1, X2))] = [2] X1 + [2] X2 + [2]        
                         > [2] X1 + [1]                 
                         = [c_5(a__eq^#(X1, X2))]       
                                                        

Hurray, we answered YES(?,O(n^1))