YES
Time: 0.000439
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()}
 DP:
  DP:
   {}
  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