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)}
 POP*:
  Quasi-Precedence:
  terms > sqr, 
  terms > recip, 
  terms > cons, 
  first > nil
  empty
  
Normal:
   pi(first) = [1,2], pi(terms) = [1], pi(sqr) = [1]
  
Safe:
   pi(recip) = [1], pi(cons) = [1]
  
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