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(X1, X2),
        activate(n__from(X)) -> from(X),
                     from(X) -> cons(X, n__from(s(X))),
                     from(X) -> n__from(X)}
 DP:
  Strict:
   {   first#(s(X), cons(Y, Z)) -> activate#(Z),
    activate#(n__first(X1, X2)) -> first#(X1, X2),
          activate#(n__from(X)) -> from#(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(X1, X2),
         activate(n__from(X)) -> from(X),
                      from(X) -> cons(X, n__from(s(X))),
                      from(X) -> n__from(X)}
  EDG:
   {(first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__from(X)) -> from#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(Z))}
   SCCS:
    Scc:
     {   first#(s(X), cons(Y, Z)) -> activate#(Z),
      activate#(n__first(X1, X2)) -> first#(X1, X2)}
    SCC:
     Strict:
      {   first#(s(X), cons(Y, Z)) -> activate#(Z),
       activate#(n__first(X1, X2)) -> first#(X1, X2)}
     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(X1, X2),
            activate(n__from(X)) -> from(X),
                         from(X) -> cons(X, n__from(s(X))),
                         from(X) -> n__from(X)}
     SPSC:
      Simple Projection:
       pi(activate#) = 0, pi(first#) = 1
      Strict:
       {first#(s(X), cons(Y, Z)) -> activate#(Z)}
      EDG:
       {}
       SCCS:
        
        Qed