YES
TRS:
 {                  from(X) -> cons(X, n__from(s(X))),
                    from(X) -> n__from(X),
          head(cons(X, XS)) -> X,
                activate(X) -> X,
       activate(n__from(X)) -> from(X),
  activate(n__take(X1, X2)) -> take(X1, X2),
           2nd(cons(X, XS)) -> head(activate(XS)),
               take(X1, X2) -> n__take(X1, X2),
    take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
              take(0(), XS) -> nil(),
     sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
      sel(0(), cons(X, XS)) -> X}
 DP:
  Strict:
   {     activate#(n__from(X)) -> from#(X),
    activate#(n__take(X1, X2)) -> take#(X1, X2),
             2nd#(cons(X, XS)) -> head#(activate(XS)),
             2nd#(cons(X, XS)) -> activate#(XS),
      take#(s(N), cons(X, XS)) -> activate#(XS),
       sel#(s(N), cons(X, XS)) -> activate#(XS),
       sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS))}
  Weak:
  {                  from(X) -> cons(X, n__from(s(X))),
                     from(X) -> n__from(X),
           head(cons(X, XS)) -> X,
                 activate(X) -> X,
        activate(n__from(X)) -> from(X),
   activate(n__take(X1, X2)) -> take(X1, X2),
            2nd(cons(X, XS)) -> head(activate(XS)),
                take(X1, X2) -> n__take(X1, X2),
     take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
               take(0(), XS) -> nil(),
      sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
       sel(0(), cons(X, XS)) -> X}
  EDG:
   {(2nd#(cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> take#(X1, X2))
    (2nd#(cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> from#(X))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> take#(X1, X2))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> from#(X))
    (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(N), cons(X, XS)) -> activate#(XS))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> from#(X))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> take#(X1, X2))
    (sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)), sel#(s(N), cons(X, XS)) -> activate#(XS))
    (sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)), sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)))}
   SCCS:
    Scc:
     {sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS))}
    Scc:
     {activate#(n__take(X1, X2)) -> take#(X1, X2),
        take#(s(N), cons(X, XS)) -> activate#(XS)}
    SCC:
     Strict:
      {sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS))}
     Weak:
     {                  from(X) -> cons(X, n__from(s(X))),
                        from(X) -> n__from(X),
              head(cons(X, XS)) -> X,
                    activate(X) -> X,
           activate(n__from(X)) -> from(X),
      activate(n__take(X1, X2)) -> take(X1, X2),
               2nd(cons(X, XS)) -> head(activate(XS)),
                   take(X1, X2) -> n__take(X1, X2),
        take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                  take(0(), XS) -> nil(),
         sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
          sel(0(), cons(X, XS)) -> X}
     SPSC:
      Simple Projection:
       pi(sel#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {activate#(n__take(X1, X2)) -> take#(X1, X2),
         take#(s(N), cons(X, XS)) -> activate#(XS)}
     Weak:
     {                  from(X) -> cons(X, n__from(s(X))),
                        from(X) -> n__from(X),
              head(cons(X, XS)) -> X,
                    activate(X) -> X,
           activate(n__from(X)) -> from(X),
      activate(n__take(X1, X2)) -> take(X1, X2),
               2nd(cons(X, XS)) -> head(activate(XS)),
                   take(X1, X2) -> n__take(X1, X2),
        take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                  take(0(), XS) -> nil(),
         sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
          sel(0(), cons(X, XS)) -> X}
     SPSC:
      Simple Projection:
       pi(take#) = 1, pi(activate#) = 0
      Strict:
       {take#(s(N), cons(X, XS)) -> activate#(XS)}
      EDG:
       {}
       SCCS:
        
        Qed