TRS:
 {             first(0(), X) -> nil(),
     first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                     from(X) -> cons(X, n__from(s(X))),
               first(X1, X2) -> n__first(X1, X2),
                     from(X) -> n__from(X),
  activate(n__first(X1, X2)) -> first(X1, X2),
        activate(n__from(X)) -> from(X),
                 activate(X) -> X}
 POP*:
  Quasi-Precedence:
  activate ~ first ~ from > n__from, 
  activate ~ first ~ from > s, 
  activate ~ first ~ from > n__first, 
  activate ~ first ~ from > cons, 
  activate ~ first ~ from > nil
  empty
  
Normal:
   pi(from) = [1], pi(activate) = [1], pi(first) = [1,2]
  
Safe:
   pi(n__from) = [1], pi(s) = [1], pi(n__first) = [1,2], pi(cons) = [1,2]
  
Predicative System:
   {              first(0(),X;) -> nil(),
       first(s(;X),cons(;Y,Z);) -> cons(;Y,n__first(;X,activate(Z;))),
                       from(X;) -> cons(;X,n__from(;s(;X))),
                  first(X1,X2;) -> n__first(;X1,X2),
                       from(X;) -> n__from(;X),
    activate(n__first(;X1,X2);) -> first(X1,X2;),
         activate(n__from(;X);) -> from(X;),
                   activate(X;) -> X}
  Qed