YES
Time: 0.000391
TRS:
 {     first(0(), X) -> nil(),
  first(s X, cons Y) -> cons Y,
              from X -> cons X}
 DP:
  DP:
   {}
  TRS:
  {     first(0(), X) -> nil(),
   first(s X, cons Y) -> cons Y,
               from X -> cons X}
  Qed