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