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()
 }
 Natural interpretation:
  Strict:
   {
          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()
   }
  Weak:
   {}
  Interpretation class: stronglylinear
  [len](X0) = + 1*X0 + 1
  [add](X1, X0) = + 1*X0 + 1*X1 + 1
  [from](X0) = + 1*X0 + 1
  [s] = + 0
  [cons](X0) = + 1*X0 + 0
  [0] = + 0
  [fst](X1, X0) = + 1*X0 + 1*X1 + 1
  [nil] = + 0
  
  Qed