YES
O(n)
TRS:
 {
         first(0(), X) -> nil(),
  first(s(X), cons(Y)) -> cons(Y),
               from(X) -> cons(X)
 }
 Natural interpretation:
  Strict:
   {
           first(0(), X) -> nil(),
    first(s(X), cons(Y)) -> cons(Y),
                 from(X) -> cons(X)
   }
  Weak:
   {}
  Interpretation class: stronglylinear
  [from](X0) = + 1*X0 + 1
  [s](X0) = + 1*X0 + 0
  [cons](X0) = + 1*X0 + 0
  [0] = + 0
  [first](X1, X0) = + 1*X0 + 1*X1 + 1
  [nil] = + 0
  
  Qed