TRS:
 {             zeros() -> cons(0(), n__zeros()),
     tail(cons(X, XS)) -> activate(XS),
               zeros() -> n__zeros(),
  activate(n__zeros()) -> zeros(),
           activate(X) -> X}
 LMPO:
  Quasi-Precedence:
  activate > zeros, 
  tail > activate
  empty
  
Normal:
   pi(tail) = [1], pi(activate) = [1]
  
Safe:
   
  
Predicative System:
   {              zeros() -> cons(0(),n__zeros();),
       tail(cons(X,XS;);) -> activate(XS;),
                  zeros() -> n__zeros(),
    activate(n__zeros();) -> zeros(),
             activate(X;) -> X}
  

   
  

  Qed