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