YES
TRS:
 {                  from(X) -> cons(X, n__from(n__s(X))),
                    from(X) -> n__from(X),
          head(cons(X, XS)) -> X,
                activate(X) -> X,
       activate(n__from(X)) -> from(activate(X)),
          activate(n__s(X)) -> s(activate(X)),
  activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
           2nd(cons(X, XS)) -> head(activate(XS)),
               take(X1, X2) -> n__take(X1, X2),
              take(0(), XS) -> nil(),
    take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                       s(X) -> n__s(X),
      sel(0(), cons(X, XS)) -> X,
     sel(s(N), cons(X, XS)) -> sel(N, activate(XS))}
 DP:
  Strict:
   {     activate#(n__from(X)) -> from#(activate(X)),
         activate#(n__from(X)) -> activate#(X),
            activate#(n__s(X)) -> activate#(X),
            activate#(n__s(X)) -> s#(activate(X)),
    activate#(n__take(X1, X2)) -> activate#(X1),
    activate#(n__take(X1, X2)) -> activate#(X2),
    activate#(n__take(X1, X2)) -> take#(activate(X1), activate(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(n__s(X))),
                     from(X) -> n__from(X),
           head(cons(X, XS)) -> X,
                 activate(X) -> X,
        activate(n__from(X)) -> from(activate(X)),
           activate(n__s(X)) -> s(activate(X)),
   activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
            2nd(cons(X, XS)) -> head(activate(XS)),
                take(X1, X2) -> n__take(X1, X2),
               take(0(), XS) -> nil(),
     take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                        s(X) -> n__s(X),
       sel(0(), cons(X, XS)) -> X,
      sel(s(N), cons(X, XS)) -> sel(N, activate(XS))}
  EDG:
   {(activate#(n__from(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2))
    (activate#(n__from(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1))
    (activate#(n__from(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
    (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(N), cons(X, XS)) -> activate#(XS))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> activate#(X))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> from#(activate(X)))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> activate#(X2))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> activate#(X1))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> s#(activate(X)))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> activate#(X))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> activate#(X))
    (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> from#(activate(X)))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> from#(activate(X)))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> activate#(X))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> activate#(X))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> s#(activate(X)))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> activate#(X1))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> activate#(X2))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (2nd#(cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> from#(activate(X)))
    (2nd#(cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> activate#(X))
    (2nd#(cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> activate#(X))
    (2nd#(cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> s#(activate(X)))
    (2nd#(cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> activate#(X1))
    (2nd#(cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> activate#(X2))
    (2nd#(cons(X, XS)) -> activate#(XS), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(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)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1))
    (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2))
    (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> activate#(X))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> activate#(X1))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> activate#(X2))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))}
   SCCS:
    Scc:
     {sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS))}
    Scc:
     {     activate#(n__from(X)) -> activate#(X),
              activate#(n__s(X)) -> activate#(X),
      activate#(n__take(X1, X2)) -> activate#(X1),
      activate#(n__take(X1, X2)) -> activate#(X2),
      activate#(n__take(X1, X2)) -> take#(activate(X1), activate(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(n__s(X))),
                        from(X) -> n__from(X),
              head(cons(X, XS)) -> X,
                    activate(X) -> X,
           activate(n__from(X)) -> from(activate(X)),
              activate(n__s(X)) -> s(activate(X)),
      activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
               2nd(cons(X, XS)) -> head(activate(XS)),
                   take(X1, X2) -> n__take(X1, X2),
                  take(0(), XS) -> nil(),
        take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                           s(X) -> n__s(X),
          sel(0(), cons(X, XS)) -> X,
         sel(s(N), cons(X, XS)) -> sel(N, activate(XS))}
     SPSC:
      Simple Projection:
       pi(sel#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {     activate#(n__from(X)) -> activate#(X),
               activate#(n__s(X)) -> activate#(X),
       activate#(n__take(X1, X2)) -> activate#(X1),
       activate#(n__take(X1, X2)) -> activate#(X2),
       activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)),
         take#(s(N), cons(X, XS)) -> activate#(XS)}
     Weak:
     {                  from(X) -> cons(X, n__from(n__s(X))),
                        from(X) -> n__from(X),
              head(cons(X, XS)) -> X,
                    activate(X) -> X,
           activate(n__from(X)) -> from(activate(X)),
              activate(n__s(X)) -> s(activate(X)),
      activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
               2nd(cons(X, XS)) -> head(activate(XS)),
                   take(X1, X2) -> n__take(X1, X2),
                  take(0(), XS) -> nil(),
        take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                           s(X) -> n__s(X),
          sel(0(), cons(X, XS)) -> X,
         sel(s(N), cons(X, XS)) -> sel(N, activate(XS))}
     POLY:
      Argument Filtering:
       pi(sel) = [], pi(s) = 0, pi(n__take) = [0,1], pi(0) = [], pi(take#) = [1], pi(take) = [0,1], pi(nil) = [], pi(2nd) = [], pi(activate#) = [0], pi(activate) = 0, pi(head) = [], pi(from) = 0, pi(n__s) = 0, pi(n__from) = 0, pi(cons) = 1
      Usable Rules:
       {}
      Interpretation:
       [take#](x0) = x0 + 1,
       [activate#](x0) = x0 + 1,
       [n__take](x0, x1) = x0 + x1 + 1
      Strict:
       {   activate#(n__from(X)) -> activate#(X),
              activate#(n__s(X)) -> activate#(X),
        take#(s(N), cons(X, XS)) -> activate#(XS)}
      Weak:
       {                  from(X) -> cons(X, n__from(n__s(X))),
                          from(X) -> n__from(X),
                head(cons(X, XS)) -> X,
                      activate(X) -> X,
             activate(n__from(X)) -> from(activate(X)),
                activate(n__s(X)) -> s(activate(X)),
        activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
                 2nd(cons(X, XS)) -> head(activate(XS)),
                     take(X1, X2) -> n__take(X1, X2),
                    take(0(), XS) -> nil(),
          take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                             s(X) -> n__s(X),
            sel(0(), cons(X, XS)) -> X,
           sel(s(N), cons(X, XS)) -> sel(N, activate(XS))}
      EDG:
       {(activate#(n__from(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
        (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
        (activate#(n__s(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
        (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
        (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> activate#(X))
        (take#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> activate#(X))}
       SCCS:
        Scc:
         {activate#(n__from(X)) -> activate#(X),
             activate#(n__s(X)) -> activate#(X)}
        SCC:
         Strict:
          {activate#(n__from(X)) -> activate#(X),
              activate#(n__s(X)) -> activate#(X)}
         Weak:
         {                  from(X) -> cons(X, n__from(n__s(X))),
                            from(X) -> n__from(X),
                  head(cons(X, XS)) -> X,
                        activate(X) -> X,
               activate(n__from(X)) -> from(activate(X)),
                  activate(n__s(X)) -> s(activate(X)),
          activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
                   2nd(cons(X, XS)) -> head(activate(XS)),
                       take(X1, X2) -> n__take(X1, X2),
                      take(0(), XS) -> nil(),
            take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                               s(X) -> n__s(X),
              sel(0(), cons(X, XS)) -> X,
             sel(s(N), cons(X, XS)) -> sel(N, activate(XS))}
         SPSC:
          Simple Projection:
           pi(activate#) = 0
          Strict:
           {activate#(n__s(X)) -> activate#(X)}
          EDG:
           {(activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))}
           SCCS:
            Scc:
             {activate#(n__s(X)) -> activate#(X)}
            SCC:
             Strict:
              {activate#(n__s(X)) -> activate#(X)}
             Weak:
             {                  from(X) -> cons(X, n__from(n__s(X))),
                                from(X) -> n__from(X),
                      head(cons(X, XS)) -> X,
                            activate(X) -> X,
                   activate(n__from(X)) -> from(activate(X)),
                      activate(n__s(X)) -> s(activate(X)),
              activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
                       2nd(cons(X, XS)) -> head(activate(XS)),
                           take(X1, X2) -> n__take(X1, X2),
                          take(0(), XS) -> nil(),
                take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))),
                                   s(X) -> n__s(X),
                  sel(0(), cons(X, XS)) -> X,
                 sel(s(N), cons(X, XS)) -> sel(N, activate(XS))}
             SPSC:
              Simple Projection:
               pi(activate#) = 0
              Strict:
               {}
              Qed