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