YES

Problem:
 a__eq(0(),0()) -> true()
 a__eq(s(X),s(Y)) -> a__eq(X,Y)
 a__eq(X,Y) -> false()
 a__inf(X) -> cons(X,inf(s(X)))
 a__take(0(),X) -> nil()
 a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
 a__length(nil()) -> 0()
 a__length(cons(X,L)) -> s(length(L))
 mark(eq(X1,X2)) -> a__eq(X1,X2)
 mark(inf(X)) -> a__inf(mark(X))
 mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
 mark(length(X)) -> a__length(mark(X))
 mark(0()) -> 0()
 mark(true()) -> true()
 mark(s(X)) -> s(X)
 mark(false()) -> false()
 mark(cons(X1,X2)) -> cons(X1,X2)
 mark(nil()) -> nil()
 a__eq(X1,X2) -> eq(X1,X2)
 a__inf(X) -> inf(X)
 a__take(X1,X2) -> take(X1,X2)
 a__length(X) -> length(X)

Proof:
 DP Processor:
  DPs:
   a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
   mark#(eq(X1,X2)) -> a__eq#(X1,X2)
   mark#(inf(X)) -> mark#(X)
   mark#(inf(X)) -> a__inf#(mark(X))
   mark#(take(X1,X2)) -> mark#(X2)
   mark#(take(X1,X2)) -> mark#(X1)
   mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
   mark#(length(X)) -> mark#(X)
   mark#(length(X)) -> a__length#(mark(X))
  TRS:
   a__eq(0(),0()) -> true()
   a__eq(s(X),s(Y)) -> a__eq(X,Y)
   a__eq(X,Y) -> false()
   a__inf(X) -> cons(X,inf(s(X)))
   a__take(0(),X) -> nil()
   a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
   a__length(nil()) -> 0()
   a__length(cons(X,L)) -> s(length(L))
   mark(eq(X1,X2)) -> a__eq(X1,X2)
   mark(inf(X)) -> a__inf(mark(X))
   mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
   mark(length(X)) -> a__length(mark(X))
   mark(0()) -> 0()
   mark(true()) -> true()
   mark(s(X)) -> s(X)
   mark(false()) -> false()
   mark(cons(X1,X2)) -> cons(X1,X2)
   mark(nil()) -> nil()
   a__eq(X1,X2) -> eq(X1,X2)
   a__inf(X) -> inf(X)
   a__take(X1,X2) -> take(X1,X2)
   a__length(X) -> length(X)
  EDG Processor:
   DPs:
    a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
    mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(inf(X)) -> mark#(X)
    mark#(inf(X)) -> a__inf#(mark(X))
    mark#(take(X1,X2)) -> mark#(X2)
    mark#(take(X1,X2)) -> mark#(X1)
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(length(X)) -> mark#(X)
    mark#(length(X)) -> a__length#(mark(X))
   TRS:
    a__eq(0(),0()) -> true()
    a__eq(s(X),s(Y)) -> a__eq(X,Y)
    a__eq(X,Y) -> false()
    a__inf(X) -> cons(X,inf(s(X)))
    a__take(0(),X) -> nil()
    a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
    a__length(nil()) -> 0()
    a__length(cons(X,L)) -> s(length(L))
    mark(eq(X1,X2)) -> a__eq(X1,X2)
    mark(inf(X)) -> a__inf(mark(X))
    mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
    mark(length(X)) -> a__length(mark(X))
    mark(0()) -> 0()
    mark(true()) -> true()
    mark(s(X)) -> s(X)
    mark(false()) -> false()
    mark(cons(X1,X2)) -> cons(X1,X2)
    mark(nil()) -> nil()
    a__eq(X1,X2) -> eq(X1,X2)
    a__inf(X) -> inf(X)
    a__take(X1,X2) -> take(X1,X2)
    a__length(X) -> length(X)
   graph:
    mark#(eq(X1,X2)) -> a__eq#(X1,X2) ->
    a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
    mark#(length(X)) -> mark#(X) -> mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(length(X)) -> mark#(X) -> mark#(inf(X)) -> mark#(X)
    mark#(length(X)) -> mark#(X) -> mark#(inf(X)) -> a__inf#(mark(X))
    mark#(length(X)) -> mark#(X) -> mark#(take(X1,X2)) -> mark#(X2)
    mark#(length(X)) -> mark#(X) -> mark#(take(X1,X2)) -> mark#(X1)
    mark#(length(X)) -> mark#(X) ->
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(length(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X)
    mark#(length(X)) -> mark#(X) ->
    mark#(length(X)) -> a__length#(mark(X))
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(take(X1,X2)) -> mark#(X2) -> mark#(inf(X)) -> mark#(X)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(inf(X)) -> a__inf#(mark(X))
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(take(X1,X2)) -> mark#(X2)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(take(X1,X2)) -> mark#(X1)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(take(X1,X2)) -> mark#(X2) -> mark#(length(X)) -> mark#(X)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(length(X)) -> a__length#(mark(X))
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(take(X1,X2)) -> mark#(X1) -> mark#(inf(X)) -> mark#(X)
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(inf(X)) -> a__inf#(mark(X))
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(take(X1,X2)) -> mark#(X2)
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(take(X1,X2)) -> mark#(X1)
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(take(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> a__length#(mark(X))
    mark#(inf(X)) -> mark#(X) -> mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(inf(X)) -> mark#(X) -> mark#(inf(X)) -> mark#(X)
    mark#(inf(X)) -> mark#(X) -> mark#(inf(X)) -> a__inf#(mark(X))
    mark#(inf(X)) -> mark#(X) -> mark#(take(X1,X2)) -> mark#(X2)
    mark#(inf(X)) -> mark#(X) -> mark#(take(X1,X2)) -> mark#(X1)
    mark#(inf(X)) -> mark#(X) ->
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(inf(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X)
    mark#(inf(X)) -> mark#(X) ->
    mark#(length(X)) -> a__length#(mark(X))
    a__eq#(s(X),s(Y)) -> a__eq#(X,Y) -> a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 34/81
    DPs:
     mark#(length(X)) -> mark#(X)
     mark#(take(X1,X2)) -> mark#(X1)
     mark#(take(X1,X2)) -> mark#(X2)
     mark#(inf(X)) -> mark#(X)
    TRS:
     a__eq(0(),0()) -> true()
     a__eq(s(X),s(Y)) -> a__eq(X,Y)
     a__eq(X,Y) -> false()
     a__inf(X) -> cons(X,inf(s(X)))
     a__take(0(),X) -> nil()
     a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
     a__length(nil()) -> 0()
     a__length(cons(X,L)) -> s(length(L))
     mark(eq(X1,X2)) -> a__eq(X1,X2)
     mark(inf(X)) -> a__inf(mark(X))
     mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
     mark(length(X)) -> a__length(mark(X))
     mark(0()) -> 0()
     mark(true()) -> true()
     mark(s(X)) -> s(X)
     mark(false()) -> false()
     mark(cons(X1,X2)) -> cons(X1,X2)
     mark(nil()) -> nil()
     a__eq(X1,X2) -> eq(X1,X2)
     a__inf(X) -> inf(X)
     a__take(X1,X2) -> take(X1,X2)
     a__length(X) -> length(X)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [mark#](x0) = x0,
      
      [mark](x0) = x0,
      
      [eq](x0, x1) = 0,
      
      [length](x0) = x0,
      
      [a__length](x0) = x0,
      
      [take](x0, x1) = x0 + x1,
      
      [nil] = 0,
      
      [a__take](x0, x1) = x0 + x1,
      
      [cons](x0, x1) = 0,
      
      [inf](x0) = x0 + 1,
      
      [a__inf](x0) = x0 + 1,
      
      [false] = 0,
      
      [s](x0) = 0,
      
      [true] = 0,
      
      [a__eq](x0, x1) = 0,
      
      [0] = 0
     orientation:
      mark#(length(X)) = X >= X = mark#(X)
      
      mark#(take(X1,X2)) = X1 + X2 >= X1 = mark#(X1)
      
      mark#(take(X1,X2)) = X1 + X2 >= X2 = mark#(X2)
      
      mark#(inf(X)) = X + 1 >= X = mark#(X)
      
      a__eq(0(),0()) = 0 >= 0 = true()
      
      a__eq(s(X),s(Y)) = 0 >= 0 = a__eq(X,Y)
      
      a__eq(X,Y) = 0 >= 0 = false()
      
      a__inf(X) = X + 1 >= 0 = cons(X,inf(s(X)))
      
      a__take(0(),X) = X >= 0 = nil()
      
      a__take(s(X),cons(Y,L)) = 0 >= 0 = cons(Y,take(X,L))
      
      a__length(nil()) = 0 >= 0 = 0()
      
      a__length(cons(X,L)) = 0 >= 0 = s(length(L))
      
      mark(eq(X1,X2)) = 0 >= 0 = a__eq(X1,X2)
      
      mark(inf(X)) = X + 1 >= X + 1 = a__inf(mark(X))
      
      mark(take(X1,X2)) = X1 + X2 >= X1 + X2 = a__take(mark(X1),mark(X2))
      
      mark(length(X)) = X >= X = a__length(mark(X))
      
      mark(0()) = 0 >= 0 = 0()
      
      mark(true()) = 0 >= 0 = true()
      
      mark(s(X)) = 0 >= 0 = s(X)
      
      mark(false()) = 0 >= 0 = false()
      
      mark(cons(X1,X2)) = 0 >= 0 = cons(X1,X2)
      
      mark(nil()) = 0 >= 0 = nil()
      
      a__eq(X1,X2) = 0 >= 0 = eq(X1,X2)
      
      a__inf(X) = X + 1 >= X + 1 = inf(X)
      
      a__take(X1,X2) = X1 + X2 >= X1 + X2 = take(X1,X2)
      
      a__length(X) = X >= X = length(X)
     problem:
      DPs:
       mark#(length(X)) -> mark#(X)
       mark#(take(X1,X2)) -> mark#(X1)
       mark#(take(X1,X2)) -> mark#(X2)
      TRS:
       a__eq(0(),0()) -> true()
       a__eq(s(X),s(Y)) -> a__eq(X,Y)
       a__eq(X,Y) -> false()
       a__inf(X) -> cons(X,inf(s(X)))
       a__take(0(),X) -> nil()
       a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
       a__length(nil()) -> 0()
       a__length(cons(X,L)) -> s(length(L))
       mark(eq(X1,X2)) -> a__eq(X1,X2)
       mark(inf(X)) -> a__inf(mark(X))
       mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
       mark(length(X)) -> a__length(mark(X))
       mark(0()) -> 0()
       mark(true()) -> true()
       mark(s(X)) -> s(X)
       mark(false()) -> false()
       mark(cons(X1,X2)) -> cons(X1,X2)
       mark(nil()) -> nil()
       a__eq(X1,X2) -> eq(X1,X2)
       a__inf(X) -> inf(X)
       a__take(X1,X2) -> take(X1,X2)
       a__length(X) -> length(X)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [mark#](x0) = x0 + 1,
       
       [mark](x0) = x0,
       
       [eq](x0, x1) = 0,
       
       [length](x0) = x0 + 1,
       
       [a__length](x0) = x0 + 1,
       
       [take](x0, x1) = x0 + x1 + 1,
       
       [nil] = 1,
       
       [a__take](x0, x1) = x0 + x1 + 1,
       
       [cons](x0, x1) = x1,
       
       [inf](x0) = 0,
       
       [a__inf](x0) = 0,
       
       [false] = 0,
       
       [s](x0) = x0,
       
       [true] = 0,
       
       [a__eq](x0, x1) = 0,
       
       [0] = 0
      orientation:
       mark#(length(X)) = X + 2 >= X + 1 = mark#(X)
       
       mark#(take(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = mark#(X1)
       
       mark#(take(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = mark#(X2)
       
       a__eq(0(),0()) = 0 >= 0 = true()
       
       a__eq(s(X),s(Y)) = 0 >= 0 = a__eq(X,Y)
       
       a__eq(X,Y) = 0 >= 0 = false()
       
       a__inf(X) = 0 >= 0 = cons(X,inf(s(X)))
       
       a__take(0(),X) = X + 1 >= 1 = nil()
       
       a__take(s(X),cons(Y,L)) = L + X + 1 >= L + X + 1 = cons(Y,take(X,L))
       
       a__length(nil()) = 2 >= 0 = 0()
       
       a__length(cons(X,L)) = L + 1 >= L + 1 = s(length(L))
       
       mark(eq(X1,X2)) = 0 >= 0 = a__eq(X1,X2)
       
       mark(inf(X)) = 0 >= 0 = a__inf(mark(X))
       
       mark(take(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = a__take(mark(X1),mark(X2))
       
       mark(length(X)) = X + 1 >= X + 1 = a__length(mark(X))
       
       mark(0()) = 0 >= 0 = 0()
       
       mark(true()) = 0 >= 0 = true()
       
       mark(s(X)) = X >= X = s(X)
       
       mark(false()) = 0 >= 0 = false()
       
       mark(cons(X1,X2)) = X2 >= X2 = cons(X1,X2)
       
       mark(nil()) = 1 >= 1 = nil()
       
       a__eq(X1,X2) = 0 >= 0 = eq(X1,X2)
       
       a__inf(X) = 0 >= 0 = inf(X)
       
       a__take(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 1 = take(X1,X2)
       
       a__length(X) = X + 1 >= X + 1 = length(X)
      problem:
       DPs:
        
       TRS:
        a__eq(0(),0()) -> true()
        a__eq(s(X),s(Y)) -> a__eq(X,Y)
        a__eq(X,Y) -> false()
        a__inf(X) -> cons(X,inf(s(X)))
        a__take(0(),X) -> nil()
        a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
        a__length(nil()) -> 0()
        a__length(cons(X,L)) -> s(length(L))
        mark(eq(X1,X2)) -> a__eq(X1,X2)
        mark(inf(X)) -> a__inf(mark(X))
        mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
        mark(length(X)) -> a__length(mark(X))
        mark(0()) -> 0()
        mark(true()) -> true()
        mark(s(X)) -> s(X)
        mark(false()) -> false()
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(nil()) -> nil()
        a__eq(X1,X2) -> eq(X1,X2)
        a__inf(X) -> inf(X)
        a__take(X1,X2) -> take(X1,X2)
        a__length(X) -> length(X)
      Qed
    
    DPs:
     a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
    TRS:
     a__eq(0(),0()) -> true()
     a__eq(s(X),s(Y)) -> a__eq(X,Y)
     a__eq(X,Y) -> false()
     a__inf(X) -> cons(X,inf(s(X)))
     a__take(0(),X) -> nil()
     a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
     a__length(nil()) -> 0()
     a__length(cons(X,L)) -> s(length(L))
     mark(eq(X1,X2)) -> a__eq(X1,X2)
     mark(inf(X)) -> a__inf(mark(X))
     mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
     mark(length(X)) -> a__length(mark(X))
     mark(0()) -> 0()
     mark(true()) -> true()
     mark(s(X)) -> s(X)
     mark(false()) -> false()
     mark(cons(X1,X2)) -> cons(X1,X2)
     mark(nil()) -> nil()
     a__eq(X1,X2) -> eq(X1,X2)
     a__inf(X) -> inf(X)
     a__take(X1,X2) -> take(X1,X2)
     a__length(X) -> length(X)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [a__eq#](x0, x1) = x1 + 1,
      
      [mark](x0) = x0 + 1,
      
      [eq](x0, x1) = 0,
      
      [length](x0) = 0,
      
      [a__length](x0) = 1,
      
      [take](x0, x1) = x1,
      
      [nil] = 0,
      
      [a__take](x0, x1) = x1,
      
      [cons](x0, x1) = 1,
      
      [inf](x0) = 0,
      
      [a__inf](x0) = 1,
      
      [false] = 1,
      
      [s](x0) = x0 + 1,
      
      [true] = 1,
      
      [a__eq](x0, x1) = 1,
      
      [0] = 1
     orientation:
      a__eq#(s(X),s(Y)) = Y + 2 >= Y + 1 = a__eq#(X,Y)
      
      a__eq(0(),0()) = 1 >= 1 = true()
      
      a__eq(s(X),s(Y)) = 1 >= 1 = a__eq(X,Y)
      
      a__eq(X,Y) = 1 >= 1 = false()
      
      a__inf(X) = 1 >= 1 = cons(X,inf(s(X)))
      
      a__take(0(),X) = X >= 0 = nil()
      
      a__take(s(X),cons(Y,L)) = 1 >= 1 = cons(Y,take(X,L))
      
      a__length(nil()) = 1 >= 1 = 0()
      
      a__length(cons(X,L)) = 1 >= 1 = s(length(L))
      
      mark(eq(X1,X2)) = 1 >= 1 = a__eq(X1,X2)
      
      mark(inf(X)) = 1 >= 1 = a__inf(mark(X))
      
      mark(take(X1,X2)) = X2 + 1 >= X2 + 1 = a__take(mark(X1),mark(X2))
      
      mark(length(X)) = 1 >= 1 = a__length(mark(X))
      
      mark(0()) = 2 >= 1 = 0()
      
      mark(true()) = 2 >= 1 = true()
      
      mark(s(X)) = X + 2 >= X + 1 = s(X)
      
      mark(false()) = 2 >= 1 = false()
      
      mark(cons(X1,X2)) = 2 >= 1 = cons(X1,X2)
      
      mark(nil()) = 1 >= 0 = nil()
      
      a__eq(X1,X2) = 1 >= 0 = eq(X1,X2)
      
      a__inf(X) = 1 >= 0 = inf(X)
      
      a__take(X1,X2) = X2 >= X2 = take(X1,X2)
      
      a__length(X) = 1 >= 0 = length(X)
     problem:
      DPs:
       
      TRS:
       a__eq(0(),0()) -> true()
       a__eq(s(X),s(Y)) -> a__eq(X,Y)
       a__eq(X,Y) -> false()
       a__inf(X) -> cons(X,inf(s(X)))
       a__take(0(),X) -> nil()
       a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
       a__length(nil()) -> 0()
       a__length(cons(X,L)) -> s(length(L))
       mark(eq(X1,X2)) -> a__eq(X1,X2)
       mark(inf(X)) -> a__inf(mark(X))
       mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
       mark(length(X)) -> a__length(mark(X))
       mark(0()) -> 0()
       mark(true()) -> true()
       mark(s(X)) -> s(X)
       mark(false()) -> false()
       mark(cons(X1,X2)) -> cons(X1,X2)
       mark(nil()) -> nil()
       a__eq(X1,X2) -> eq(X1,X2)
       a__inf(X) -> inf(X)
       a__take(X1,X2) -> take(X1,X2)
       a__length(X) -> length(X)
     Qed