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())
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [zWadr#](x0, x1) = x0 + 1x1 + 0,
    
    [app#](x0, x1) = x1 + 0,
    
    [prefix](x0) = 1x0 + 8,
    
    [zWadr](x0, x1) = 1x0 + 1x1 + 0,
    
    [from](x0) = x0 + 1,
    
    [cons](x0) = 0,
    
    [app](x0, x1) = 4x0 + 2x1 + 0,
    
    [nil] = 0
   orientation:
    zWadr#(cons(X),cons(Y)) = 1 >= 0 = app#(Y,cons(X))
    
    app(nil(),YS) = 2YS + 4 >= YS = YS
    
    app(cons(X),YS) = 2YS + 4 >= 0 = cons(X)
    
    from(X) = X + 1 >= 0 = cons(X)
    
    zWadr(nil(),YS) = 1YS + 1 >= 0 = nil()
    
    zWadr(XS,nil()) = 1XS + 1 >= 0 = nil()
    
    zWadr(cons(X),cons(Y)) = 1 >= 0 = cons(app(Y,cons(X)))
    
    prefix(L) = 1L + 8 >= 0 = cons(nil())
   problem:
    DPs:
     
    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())
   Qed