YES(?,O(n^1))
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()
   }
  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 + 7
   [add](X1, X0) = + 1*X0 + 1*X1 + 7
   [from](X0) = + 1*X0 + 2
   [s] = + 7
   [cons](X0) = + 1*X0 + 1
   [0] = + 7
   [fst](X1, X0) = + 1*X0 + 1*X1 + 2
   [nil] = + 1
   
   Qed