YES
Time: 0.029496
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:
  DP:
   {  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)}
  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)}
  UR:
   {             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),
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {(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)
     (a__eq#(s X, s Y) -> a__eq#(X, Y), a__eq#(s X, s Y) -> a__eq#(X, Y))
     (mark# take(X1, X2) -> mark# X1, mark# eq(X1, X2) -> a__eq#(X1, 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# 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# inf X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# inf X -> a__inf# mark X)
     (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))
     (mark# eq(X1, X2) -> a__eq#(X1, X2), a__eq#(s X, s Y) -> a__eq#(X, Y))
     (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))}
    STATUS:
     arrows: 0.580247
     SCCS (2):
      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 (4):
       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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [a__eq](x0, x1) = x0 + 1,
         
         [cons](x0, x1) = 0,
         
         [a__take](x0, x1) = 0,
         
         [take](x0, x1) = x0 + x1 + 1,
         
         [eq](x0, x1) = 0,
         
         [s](x0) = 1,
         
         [inf](x0) = x0 + 1,
         
         [a__inf](x0) = 0,
         
         [a__length](x0) = 0,
         
         [length](x0) = x0 + 1,
         
         [mark](x0) = 0,
         
         [true] = 0,
         
         [0] = 1,
         
         [false] = 0,
         
         [nil] = 0,
         
         [mark#](x0) = x0 + 1
        Strict:
         mark# length X -> mark# X
         2 + 1X >= 1 + 1X
         mark# take(X1, X2) -> mark# X2
         2 + 1X1 + 1X2 >= 1 + 1X2
         mark# take(X1, X2) -> mark# X1
         2 + 1X1 + 1X2 >= 1 + 1X1
         mark# inf X -> mark# X
         2 + 1X >= 1 + 1X
        Weak:
         mark eq(X1, X2) -> a__eq(X1, X2)
         0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
         mark length X -> a__length mark X
         0 + 0X >= 0 + 0X
         mark take(X1, X2) -> a__take(mark X1, mark X2)
         0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
         mark nil() -> nil()
         0 >= 0
         mark inf X -> a__inf mark X
         0 + 0X >= 0 + 0X
         mark cons(X1, X2) -> cons(X1, X2)
         0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
         mark false() -> false()
         0 >= 0
         mark s X -> s X
         0 + 0X >= 1 + 0X
         mark 0() -> 0()
         0 >= 1
         mark true() -> true()
         0 >= 0
         a__length nil() -> 0()
         0 >= 1
         a__length cons(X, L) -> s length L
         0 + 0X + 0L >= 1 + 0L
         a__length X -> length X
         0 + 0X >= 1 + 1X
         a__take(s X, cons(Y, L)) -> cons(Y, take(X, L))
         0 + 0X + 0Y + 0L >= 0 + 0X + 0Y + 0L
         a__take(0(), X) -> nil()
         0 + 0X >= 0
         a__take(X1, X2) -> take(X1, X2)
         0 + 0X1 + 0X2 >= 1 + 1X1 + 1X2
         a__inf X -> inf X
         0 + 0X >= 1 + 1X
         a__inf X -> cons(X, inf s X)
         0 + 0X >= 0 + 0X
         a__eq(s X, s Y) -> a__eq(X, Y)
         2 + 0X + 0Y >= 1 + 0X + 1Y
         a__eq(0(), 0()) -> true()
         2 >= 0
         a__eq(X1, X2) -> eq(X1, X2)
         1 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
         a__eq(X, Y) -> false()
         1 + 0X + 1Y >= 0
       Qed
     
     SCC (1):
      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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [a__eq](x0, x1) = x0 + 1,
        
        [cons](x0, x1) = x0 + 1,
        
        [a__take](x0, x1) = x0 + 1,
        
        [take](x0, x1) = 1,
        
        [eq](x0, x1) = 0,
        
        [s](x0) = x0 + 1,
        
        [inf](x0) = 0,
        
        [a__inf](x0) = 0,
        
        [a__length](x0) = x0 + 1,
        
        [length](x0) = 1,
        
        [mark](x0) = x0,
        
        [true] = 0,
        
        [0] = 1,
        
        [false] = 0,
        
        [nil] = 1,
        
        [a__eq#](x0, x1) = x0
       Strict:
        a__eq#(s X, s Y) -> a__eq#(X, Y)
        1 + 0X + 1Y >= 0 + 0X + 1Y
       Weak:
        mark eq(X1, X2) -> a__eq(X1, X2)
        0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
        mark length X -> a__length mark X
        1 + 0X >= 1 + 1X
        mark take(X1, X2) -> a__take(mark X1, mark X2)
        1 + 0X1 + 0X2 >= 1 + 1X1 + 0X2
        mark nil() -> nil()
        1 >= 1
        mark inf X -> a__inf mark X
        0 + 0X >= 0 + 0X
        mark cons(X1, X2) -> cons(X1, X2)
        1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
        mark false() -> false()
        0 >= 0
        mark s X -> s X
        1 + 1X >= 1 + 1X
        mark 0() -> 0()
        1 >= 1
        mark true() -> true()
        0 >= 0
        a__length nil() -> 0()
        2 >= 1
        a__length cons(X, L) -> s length L
        2 + 0X + 1L >= 2 + 0L
        a__length X -> length X
        1 + 1X >= 1 + 0X
        a__take(s X, cons(Y, L)) -> cons(Y, take(X, L))
        2 + 1X + 0Y + 0L >= 2 + 0X + 0Y + 0L
        a__take(0(), X) -> nil()
        2 + 0X >= 1
        a__take(X1, X2) -> take(X1, X2)
        1 + 1X1 + 0X2 >= 1 + 0X1 + 0X2
        a__inf X -> inf X
        0 + 0X >= 0 + 0X
        a__inf X -> cons(X, inf s X)
        0 + 0X >= 1 + 0X
        a__eq(s X, s Y) -> a__eq(X, Y)
        2 + 0X + 1Y >= 1 + 0X + 1Y
        a__eq(0(), 0()) -> true()
        2 >= 0
        a__eq(X1, X2) -> eq(X1, X2)
        1 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
        a__eq(X, Y) -> false()
        1 + 0X + 1Y >= 0
      Qed