YES(?,O(n^1))
TRS:
 {
             sqr 0() -> 0(),
             sqr s() -> s(),
             terms N -> cons recip sqr N,
             dbl 0() -> 0(),
             dbl s() -> s(),
         add(0(), X) -> X,
         add(s(), Y) -> s(),
       first(0(), X) -> nil(),
  first(s(), cons Y) -> cons Y
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
               sqr 0() -> 0(),
               sqr s() -> s(),
               terms N -> cons recip sqr N,
               dbl 0() -> 0(),
               dbl s() -> s(),
           add(0(), X) -> X,
           add(s(), Y) -> s(),
         first(0(), X) -> nil(),
    first(s(), cons Y) -> cons Y
   }
  Natural interpretation:
   Strict:
    {
                sqr 0() -> 0(),
                sqr s() -> s(),
                terms N -> cons recip sqr N,
                dbl 0() -> 0(),
                dbl s() -> s(),
            add(0(), X) -> X,
            add(s(), Y) -> s(),
          first(0(), X) -> nil(),
     first(s(), cons Y) -> cons Y
    }
   Weak:
    {}
   Interpretation class: stronglylinear
   [first](X1, X0) = + 1*X0 + 1*X1 + 7
   [add](X1, X0) = + 1*X0 + 1*X1 + 4
   [dbl](X0) = + 1*X0 + 4
   [s] = + 7
   [0] = + 1
   [terms](X0) = + 1*X0 + 6
   [sqr](X0) = + 1*X0 + 1
   [recip](X0) = + 1*X0 + 1
   [cons](X0) = + 1*X0 + 2
   [nil] = + 7
   
   Qed