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)}
 LMPO:
  Quasi-Precedence:
  terms > sqr
  empty
  
Normal:
   pi(first) = [1,2], pi(terms) = [1], pi(sqr) = [1]
  
Safe:
   
  
Predicative System:
   {           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;)}
  

   
  

  Qed