YES

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)

linear polynomial interpretations on N:

  a__eq_A(x1,x2) = 3
  a__eq#_A(x1,x2) = 6
  0_A = 1
  0#_A = 2
  true_A = 0
  true#_A = 5
  s_A(x1) = x1
  s#_A(x1) = 0
  false_A = 1
  false#_A = 0
  a__inf_A(x1) = x1 + 3
  a__inf#_A(x1) = 6
  cons_A(x1,x2) = x2
  cons#_A(x1,x2) = 1
  inf_A(x1) = x1 + 3
  inf#_A(x1) = 5
  a__take_A(x1,x2) = x1 + x2
  a__take#_A(x1,x2) = x2 + 3
  nil_A = 1
  nil#_A = 2
  take_A(x1,x2) = x1 + x2
  take#_A(x1,x2) = 2
  a__length_A(x1) = x1
  a__length#_A(x1) = 3
  length_A(x1) = x1
  length#_A(x1) = 2
  mark_A(x1) = x1
  mark#_A(x1) = x1 + 4
  eq_A(x1,x2) = 3
  eq#_A(x1,x2) = 0

precedence:

  true = take > a__eq = a__take = length > mark = eq > false = a__inf = a__length > 0 = cons = inf = nil > s