YES
O(n)
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()
 }
 DUP: We consider a non-duplicating system.
  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()
   }
  BOUND:
   Automaton:
    {
        len_0(8) -> 8,
     add_0(8, 8) -> 8,
       from_0(8) -> 8,
           s_1() -> 8,
           s_0() -> 8,
       cons_1(8) -> 8,
       cons_0(8) -> 8,
           0_1() -> 8,
           0_0() -> 8,
     fst_0(8, 8) -> 8,
         nil_1() -> 8,
         nil_0() -> 8
    }
   Strict:
    {}
   Qed