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* + Boolean Semantic Labelling:
  Normal positions:
  pi(first_sl=1) = [1,2], pi(first_sl=0) = [1,2], pi(terms_sl=1) = [1], pi(terms_sl=0) = [1], pi(sqr_sl=1) = [1], pi(sqr_sl=0) = [1]
  
Safe positions:
   pi(recip_sl=1) = [1], pi(recip_sl=0) = [1], pi(cons_sl=1) = [1], pi(cons_sl=0) = [1]
  
Precedence:
   terms_sl=0 > sqr_sl=0, 
   terms_sl=0 > recip_sl=0, 
   terms_sl=0 > cons_sl=0, 
   first_sl=0 > nil_sl=0
   empty
  
Interpretation:
   cons^(1):
   0 | 0
   1 | 0
   recip^(1):
   0 | 0
   1 | 0
   sqr^(1):
   0 | 0
   1 | 1
   terms^(1):
   0 | 0
   1 | 0
   0^(0):
    | 1
   s^(0):
    | 0
   dbl^(1):
   0 | 0
   1 | 1
   add^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 1
   nil^(0):
    | 0
   first^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   
  
Labelling:
   cons^(1):
   0 | 0
   1 | 0
   recip^(1):
   0 | 0
   1 | 0
   sqr^(1):
   0 | 0
   1 | 0
   terms^(1):
   0 | 0
   1 | 0
   0^(0):
    | 0
   s^(0):
    | 0
   dbl^(1):
   0 | 0
   1 | 0
   add^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   nil^(0):
    | 0
   first^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   
  
Labelled predicative System:
   {                     terms_sl=0(N;) -> cons_sl=0(;recip_sl=0(;sqr_sl=0(N;))),
                         terms_sl=0(N;) -> cons_sl=0(;recip_sl=0(;sqr_sl=0(N;))),
                    sqr_sl=0(0_sl=0();) -> 0_sl=0(),
                    sqr_sl=0(s_sl=0();) -> s_sl=0(),
                    dbl_sl=0(0_sl=0();) -> 0_sl=0(),
                    dbl_sl=0(s_sl=0();) -> s_sl=0(),
                  add_sl=0(0_sl=0(),X;) -> X,
                  add_sl=0(0_sl=0(),X;) -> X,
                  add_sl=0(s_sl=0(),Y;) -> s_sl=0(),
                  add_sl=0(s_sl=0(),Y;) -> s_sl=0(),
                first_sl=0(0_sl=0(),X;) -> nil_sl=0(),
                first_sl=0(0_sl=0(),X;) -> nil_sl=0(),
    first_sl=0(s_sl=0(),cons_sl=0(;Y);) -> cons_sl=0(;Y),
    first_sl=0(s_sl=0(),cons_sl=0(;Y);) -> cons_sl=0(;Y)}
  

  Qed