TRS:
 {             zeros() -> cons(0(), n__zeros()),
     tail(cons(X, XS)) -> activate(XS),
               zeros() -> n__zeros(),
  activate(n__zeros()) -> zeros(),
           activate(X) -> X}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(tail_sl=1) = [1], pi(tail_sl=0) = [1], pi(activate_sl=1) = [1], pi(activate_sl=0) = [1]
  
Safe positions:
   pi(cons_sl=1) = [1,2], pi(cons_sl=0) = [1,2]
  
Precedence:
   activate_sl=0 > zeros_sl=0, 
   zeros_sl=0 > n__zeros_sl=0, 
   zeros_sl=0 > 0_sl=0, 
   zeros_sl=0 > cons_sl=0, 
   tail_sl=0 > activate_sl=0
   empty
  
Interpretation:
   cons^(2):
   00 | 0
   01 | 1
   10 | 0
   11 | 1
   0^(0):
    | 0
   n__zeros^(0):
    | 0
   zeros^(0):
    | 0
   activate^(1):
   0 | 0
   1 | 1
   tail^(1):
   0 | 0
   1 | 1
   
  
Labelling:
   cons^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   0^(0):
    | 0
   n__zeros^(0):
    | 0
   zeros^(0):
    | 0
   activate^(1):
   0 | 0
   1 | 0
   tail^(1):
   0 | 0
   1 | 0
   
  
Labelled predicative System:
   {                   zeros_sl=0() -> cons_sl=0(;0_sl=0(),n__zeros_sl=0()),
       tail_sl=0(cons_sl=0(;X,XS);) -> activate_sl=0(XS;),
       tail_sl=0(cons_sl=0(;X,XS);) -> activate_sl=0(XS;),
       tail_sl=0(cons_sl=0(;X,XS);) -> activate_sl=0(XS;),
       tail_sl=0(cons_sl=0(;X,XS);) -> activate_sl=0(XS;),
                       zeros_sl=0() -> n__zeros_sl=0(),
    activate_sl=0(n__zeros_sl=0();) -> zeros_sl=0(),
                  activate_sl=0(X;) -> X,
                  activate_sl=0(X;) -> X}
  

  Qed