YES(?,O(n^1))
TRS:
 {
       first(0(), X) -> nil(),
  first(s X, cons Y) -> cons Y,
              from X -> cons X
 }
 DUP: We consider a non-duplicating system.
  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 + 1
   [cons](X0) = + 1*X0 + 0
   [0] = + 2
   [first](X1, X0) = + 1*X0 + 1*X1 + 0
   [nil] = + 0
   
   Qed