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())}
 MPO:
  Prec:
   zWadr > app, 
   zWadr > cons, 
   from > cons, 
   prefix > cons, 
   prefix > nil
   empty
  Strict:
   {}
   Weak:
    {}
  Qed