YES
Trs:
 {           terms(N) -> cons(recip(sqr(N))),
             sqr(0()) -> 0(),
             sqr(s()) -> s(),
             dbl(0()) -> 0(),
             dbl(s()) -> s(),
          add(0(), X) -> X,
          add(s(), Y) -> s(),
        first(0(), X) -> nil(),
  first(s(), cons(Y)) -> cons(Y)}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {    terms_0(q8) -> q8,
         recip_1(q9) -> q8,
         recip_0(q8) -> q8,
           sqr_1(q8) -> q9,
           sqr_0(q8) -> q8,
           dbl_0(q8) -> q8,
       add_0(q8, q8) -> q8,
               0_2() -> q9,
               0_1() -> q9 | q8,
               0_0() -> q8,
             nil_1() -> q8,
             nil_0() -> q8,
               s_2() -> q9,
               s_1() -> q9 | q8,
               s_0() -> q8,
     first_0(q8, q8) -> q8,
          cons_1(q8) -> q8,
          cons_0(q8) -> q8}
   Strict:
   {}
   Qed