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