YES
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(true()) -> true(),
                  mark(0()) -> 0(),
                 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)}
 DP:
  Strict:
   { a__eq#(s(X), s(Y)) -> a__eq#(X, Y),
          mark#(inf(X)) -> a__inf#(mark(X)),
          mark#(inf(X)) -> mark#(X),
    mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)),
    mark#(take(X1, X2)) -> mark#(X1),
    mark#(take(X1, X2)) -> mark#(X2),
       mark#(length(X)) -> a__length#(mark(X)),
       mark#(length(X)) -> mark#(X),
      mark#(eq(X1, X2)) -> a__eq#(X1, X2)}
  Weak:
  {              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(true()) -> true(),
                   mark(0()) -> 0(),
                  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)}
  EDG:
   {(mark#(eq(X1, X2)) -> a__eq#(X1, X2), a__eq#(s(X), s(Y)) -> a__eq#(X, Y))
    (a__eq#(s(X), s(Y)) -> a__eq#(X, Y), 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#(length(X)) -> mark#(X))
    (mark#(length(X)) -> mark#(X), mark#(length(X)) -> a__length#(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#(inf(X)) -> mark#(X))
    (mark#(length(X)) -> mark#(X), mark#(inf(X)) -> a__inf#(mark(X)))
    (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> a__inf#(mark(X)))
    (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X))
    (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(inf(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(inf(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
    (mark#(inf(X)) -> mark#(X), mark#(eq(X1, X2)) -> a__eq#(X1, X2))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> a__inf#(mark(X)))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(eq(X1, X2)) -> a__eq#(X1, X2))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(inf(X)) -> a__inf#(mark(X)))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(inf(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(eq(X1, X2)) -> a__eq#(X1, X2))}
   SCCS:
    Scc:
     {      mark#(inf(X)) -> mark#(X),
      mark#(take(X1, X2)) -> mark#(X1),
      mark#(take(X1, X2)) -> mark#(X2),
         mark#(length(X)) -> mark#(X)}
    Scc:
     {a__eq#(s(X), s(Y)) -> a__eq#(X, Y)}
    SCC:
     Strict:
      {      mark#(inf(X)) -> mark#(X),
       mark#(take(X1, X2)) -> mark#(X1),
       mark#(take(X1, X2)) -> mark#(X2),
          mark#(length(X)) -> mark#(X)}
     Weak:
     {              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(true()) -> true(),
                      mark(0()) -> 0(),
                     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)}
     SPSC:
      Simple Projection:
       pi(mark#) = 0
      Strict:
       {      mark#(inf(X)) -> mark#(X),
        mark#(take(X1, X2)) -> mark#(X1),
           mark#(length(X)) -> mark#(X)}
      EDG:
       {(mark#(inf(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
        (mark#(inf(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1))
        (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X))
        (mark#(length(X)) -> mark#(X), mark#(inf(X)) -> mark#(X))
        (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1))
        (mark#(length(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
        (mark#(take(X1, X2)) -> mark#(X1), mark#(inf(X)) -> mark#(X))
        (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1))
        (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))}
       SCCS:
        Scc:
         {      mark#(inf(X)) -> mark#(X),
          mark#(take(X1, X2)) -> mark#(X1),
             mark#(length(X)) -> mark#(X)}
        SCC:
         Strict:
          {      mark#(inf(X)) -> mark#(X),
           mark#(take(X1, X2)) -> mark#(X1),
              mark#(length(X)) -> mark#(X)}
         Weak:
         {              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(true()) -> true(),
                          mark(0()) -> 0(),
                         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)}
         SPSC:
          Simple Projection:
           pi(mark#) = 0
          Strict:
           {   mark#(inf(X)) -> mark#(X),
            mark#(length(X)) -> mark#(X)}
          EDG:
           {(mark#(length(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
            (mark#(length(X)) -> mark#(X), mark#(inf(X)) -> mark#(X))
            (mark#(inf(X)) -> mark#(X), mark#(inf(X)) -> mark#(X))
            (mark#(inf(X)) -> mark#(X), mark#(length(X)) -> mark#(X))}
           SCCS:
            Scc:
             {   mark#(inf(X)) -> mark#(X),
              mark#(length(X)) -> mark#(X)}
            SCC:
             Strict:
              {   mark#(inf(X)) -> mark#(X),
               mark#(length(X)) -> mark#(X)}
             Weak:
             {              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(true()) -> true(),
                              mark(0()) -> 0(),
                             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)}
             SPSC:
              Simple Projection:
               pi(mark#) = 0
              Strict:
               {mark#(length(X)) -> mark#(X)}
              EDG:
               {(mark#(length(X)) -> mark#(X), mark#(length(X)) -> mark#(X))}
               SCCS:
                Scc:
                 {mark#(length(X)) -> mark#(X)}
                SCC:
                 Strict:
                  {mark#(length(X)) -> mark#(X)}
                 Weak:
                 {              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(true()) -> true(),
                                  mark(0()) -> 0(),
                                 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)}
                 SPSC:
                  Simple Projection:
                   pi(mark#) = 0
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {a__eq#(s(X), s(Y)) -> a__eq#(X, Y)}
     Weak:
     {              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(true()) -> true(),
                      mark(0()) -> 0(),
                     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)}
     SPSC:
      Simple Projection:
       pi(a__eq#) = 0
      Strict:
       {}
      Qed