YES
Trs:
 {       first(0(), X) -> nil(),
  first(s(X), cons(Y)) -> cons(Y),
               from(X) -> cons(X)}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {          0_0() -> q7,
             nil_1() -> q5,
             nil_0() -> q5,
             s_0(q7) -> q6,
             s_0(q6) -> q6,
             s_0(q5) -> q6,
     first_0(q7, q7) -> q5,
     first_0(q7, q6) -> q5,
     first_0(q7, q5) -> q5,
     first_0(q6, q7) -> q5,
     first_0(q6, q6) -> q5,
     first_0(q6, q5) -> q5,
     first_0(q5, q7) -> q5,
     first_0(q5, q6) -> q5,
     first_0(q5, q5) -> q5,
          from_0(q7) -> q5,
          from_0(q6) -> q5,
          from_0(q5) -> q5,
          cons_1(q7) -> q5,
          cons_1(q6) -> q5,
          cons_1(q5) -> q5,
          cons_0(q7) -> q5,
          cons_0(q6) -> q5,
          cons_0(q5) -> q5}
   Strict:
   {}
   Qed