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