YES

Problem:
 fst(0(),Z) -> nil()
 fst(s(),cons(Y)) -> cons(Y)
 from(X) -> cons(X)
 add(0(),X) -> X
 add(s(),Y) -> s()
 len(nil()) -> 0()
 len(cons(X)) -> s()

Proof:
 DP Processor:
  DPs:
   
  TRS:
   fst(0(),Z) -> nil()
   fst(s(),cons(Y)) -> cons(Y)
   from(X) -> cons(X)
   add(0(),X) -> X
   add(s(),Y) -> s()
   len(nil()) -> 0()
   len(cons(X)) -> s()
  Qed