TRS:
 {         app(nil(), YS) -> YS,
         app(cons(X), YS) -> cons(X),
                  from(X) -> cons(X),
         zWadr(nil(), YS) -> nil(),
         zWadr(XS, nil()) -> nil(),
  zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X))),
                prefix(L) -> cons(nil())}
 LMPO:
  Quasi-Precedence:
  zWadr > app
  empty
  
Normal:
   pi(prefix) = [1], pi(zWadr) = [1,2], pi(from) = [1], pi(app) = [1,2]
  
Safe:
   
  
Predicative System:
   {           app(nil(),YS;) -> YS,
            app(cons(X;),YS;) -> cons(X;),
                     from(X;) -> cons(X;),
             zWadr(nil(),YS;) -> nil(),
             zWadr(XS,nil();) -> nil(),
    zWadr(cons(X;),cons(Y;);) -> cons(app(Y,cons(X;););),
                   prefix(L;) -> cons(nil();)}
  

   
  

  Qed