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)}
 LMPO:
  Quasi-Precedence:
  mark > a__length, 
  mark > a__take, 
  mark > a__inf, 
  mark > a__eq
  empty
  
Normal:
   pi(mark) = [1], pi(a__eq) = [1,2]
  
Safe:
   pi(a__length) = [1], pi(a__take) = [1,2], pi(a__inf) = [1]
  
Predicative System:
   {           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