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)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [mark#](x0) = x0,
    
    [a__length#](x0) = 0,
    
    [a__take#](x0, x1) = x1,
    
    [a__inf#](x0) = 0,
    
    [a__eq#](x0, x1) = x0,
    
    [mark](x0) = 4x0 + 1,
    
    [eq](x0, x1) = 2x0 + 2,
    
    [length](x0) = x0 + 1,
    
    [a__length](x0) = x0 + 2,
    
    [take](x0, x1) = x0 + 4x1 + 2,
    
    [nil] = 2,
    
    [a__take](x0, x1) = x0 + 4x1 + 2,
    
    [cons](x0, x1) = x1,
    
    [inf](x0) = 2x0 + 1,
    
    [a__inf](x0) = 2x0 + 3,
    
    [false] = 2,
    
    [s](x0) = x0 + 1,
    
    [true] = 4,
    
    [a__eq](x0, x1) = 5x0 + 2,
    
    [0] = 4
   orientation:
    a__eq#(s(X),s(Y)) = X + 1 >= X = a__eq#(X,Y)
    
    mark#(eq(X1,X2)) = 2X1 + 2 >= X1 = a__eq#(X1,X2)
    
    mark#(inf(X)) = 2X + 1 >= X = mark#(X)
    
    mark#(inf(X)) = 2X + 1 >= 0 = a__inf#(mark(X))
    
    mark#(take(X1,X2)) = X1 + 4X2 + 2 >= X2 = mark#(X2)
    
    mark#(take(X1,X2)) = X1 + 4X2 + 2 >= X1 = mark#(X1)
    
    mark#(take(X1,X2)) = X1 + 4X2 + 2 >= 4X2 + 1 = a__take#(mark(X1),mark(X2))
    
    mark#(length(X)) = X + 1 >= X = mark#(X)
    
    mark#(length(X)) = X + 1 >= 0 = a__length#(mark(X))
    
    a__eq(0(),0()) = 22 >= 4 = true()
    
    a__eq(s(X),s(Y)) = 5X + 7 >= 5X + 2 = a__eq(X,Y)
    
    a__eq(X,Y) = 5X + 2 >= 2 = false()
    
    a__inf(X) = 2X + 3 >= 2X + 3 = cons(X,inf(s(X)))
    
    a__take(0(),X) = 4X + 6 >= 2 = nil()
    
    a__take(s(X),cons(Y,L)) = 4L + X + 3 >= 4L + X + 2 = cons(Y,take(X,L))
    
    a__length(nil()) = 4 >= 4 = 0()
    
    a__length(cons(X,L)) = L + 2 >= L + 2 = s(length(L))
    
    mark(eq(X1,X2)) = 8X1 + 9 >= 5X1 + 2 = a__eq(X1,X2)
    
    mark(inf(X)) = 8X + 5 >= 8X + 5 = a__inf(mark(X))
    
    mark(take(X1,X2)) = 4X1 + 16X2 + 9 >= 4X1 + 16X2 + 7 = a__take(mark(X1),mark(X2))
    
    mark(length(X)) = 4X + 5 >= 4X + 3 = a__length(mark(X))
    
    mark(0()) = 17 >= 4 = 0()
    
    mark(true()) = 17 >= 4 = true()
    
    mark(s(X)) = 4X + 5 >= X + 1 = s(X)
    
    mark(false()) = 9 >= 2 = false()
    
    mark(cons(X1,X2)) = 4X2 + 1 >= X2 = cons(X1,X2)
    
    mark(nil()) = 9 >= 2 = nil()
    
    a__eq(X1,X2) = 5X1 + 2 >= 2X1 + 2 = eq(X1,X2)
    
    a__inf(X) = 2X + 3 >= 2X + 1 = inf(X)
    
    a__take(X1,X2) = X1 + 4X2 + 2 >= X1 + 4X2 + 2 = take(X1,X2)
    
    a__length(X) = X + 2 >= 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