YES(?,O(n^1))
TRS:
 {
         app(nil(), YS) -> YS,
        app(cons X, YS) -> cons X,
                 from X -> cons X,
       zWadr(XS, nil()) -> nil(),
       zWadr(nil(), YS) -> nil(),
  zWadr(cons X, cons Y) -> cons app(Y, cons X),
               prefix L -> cons nil()
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
           app(nil(), YS) -> YS,
          app(cons X, YS) -> cons X,
                   from X -> cons X,
         zWadr(XS, nil()) -> nil(),
         zWadr(nil(), YS) -> nil(),
    zWadr(cons X, cons Y) -> cons app(Y, cons X),
                 prefix L -> cons nil()
   }
  Natural interpretation:
   Strict:
    {
            app(nil(), YS) -> YS,
           app(cons X, YS) -> cons X,
                    from X -> cons X,
          zWadr(XS, nil()) -> nil(),
          zWadr(nil(), YS) -> nil(),
     zWadr(cons X, cons Y) -> cons app(Y, cons X),
                  prefix L -> cons nil()
    }
   Weak:
    {}
   Interpretation class: stronglylinear
   [prefix](X0) = + 1*X0 + 7
   [zWadr](X1, X0) = + 1*X0 + 1*X1 + 7
   [from](X0) = + 1*X0 + 4
   [cons](X0) = + 1*X0 + 3
   [app](X1, X0) = + 1*X0 + 1*X1 + 4
   [nil] = + 3
   
   Qed