YES
O(n^2)
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: deltarestricted
  [len](delta, X0) = + 1*X0 + 0 + 1*X0*delta + 0*delta
  [add](delta, X1, X0) = + 1*X0 + 1*X1 + 0 + 0*X0*delta + 1*X1*delta + 0*delta
  [from](delta, X0) = + 0*X0 + 1 + 1*X0*delta + 1*delta
  [s](delta) = + 1 + 0*delta
  [cons](delta, X0) = + 0*X0 + 1 + 1*X0*delta + 0*delta
  [0](delta) = + 1 + 1*delta
  [fst](delta, X1, X0) = + 0*X0 + 1*X1 + 0 + 1*X0*delta + 1*X1*delta + 1*delta
  [nil](delta) = + 1 + 1*delta
  len_tau_1(delta) = delta/(1 + 1 * delta)
  add_tau_1(delta) = delta/(1 + 1 * delta)add_tau_2(delta) = delta/(1 + 0 * delta)
  from_tau_1(delta) = delta/(0 + 1 * delta)
  
  cons_tau_1(delta) = delta/(0 + 1 * delta)
  
  fst_tau_1(delta) = delta/(1 + 1 * delta)fst_tau_2(delta) = delta/(0 + 1 * delta)
  
  
  Qed