YES

Problem:
 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())

Proof:
 DP Processor:
  DPs:
   zWadr#(cons(X),cons(Y)) -> app#(Y,cons(X))
  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())
  Usable Rule Processor:
   DPs:
    zWadr#(cons(X),cons(Y)) -> app#(Y,cons(X))
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [zWadr#](x0, x1) = 2x1 + -8,
     
     [app#](x0, x1) = x0,
     
     [cons](x0) = x0 + -8
    orientation:
     zWadr#(cons(X),cons(Y)) = 2Y + -6 >= Y = app#(Y,cons(X))
    problem:
     DPs:
      
     TRS:
      
    Qed