YES

TRS:

  a__app(nil(),YS) -> mark(YS)
  a__app(cons(X,XS),YS) -> cons(mark(X),app(XS,YS))
  a__from(X) -> cons(mark(X),from(s(X)))
  a__zWadr(nil(),YS) -> nil()
  a__zWadr(XS,nil()) -> nil()
  a__zWadr(cons(X,XS),cons(Y,YS)) -> cons(a__app(mark(Y),cons(mark(X),nil())),zWadr(XS,YS))
  a__prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
  mark(app(X1,X2)) -> a__app(mark(X1),mark(X2))
  mark(from(X)) -> a__from(mark(X))
  mark(zWadr(X1,X2)) -> a__zWadr(mark(X1),mark(X2))
  mark(prefix(X)) -> a__prefix(mark(X))
  mark(nil()) -> nil()
  mark(cons(X1,X2)) -> cons(mark(X1),X2)
  mark(s(X)) -> s(mark(X))
  a__app(X1,X2) -> app(X1,X2)
  a__from(X) -> from(X)
  a__zWadr(X1,X2) -> zWadr(X1,X2)
  a__prefix(X) -> prefix(X)

linear polynomial interpretations on N:

  a__app_A(x1,x2) = x1 + x2 + 1
  a__app#_A(x1,x2) = x1 + x2 + 1
  nil_A = 0
  nil#_A = 0
  mark_A(x1) = x1
  mark#_A(x1) = x1 + 1
  cons_A(x1,x2) = x1
  cons#_A(x1,x2) = 1
  app_A(x1,x2) = x1 + x2 + 1
  app#_A(x1,x2) = 1
  a__from_A(x1) = x1 + 3
  a__from#_A(x1) = x1 + 3
  from_A(x1) = x1 + 3
  from#_A(x1) = x1 + 2
  s_A(x1) = x1
  s#_A(x1) = 0
  a__zWadr_A(x1,x2) = x1 + x2 + 1
  a__zWadr#_A(x1,x2) = x1 + x2 + 1
  zWadr_A(x1,x2) = x1 + x2 + 1
  zWadr#_A(x1,x2) = 0
  a__prefix_A(x1) = x1 + 2
  a__prefix#_A(x1) = 2
  prefix_A(x1) = x1 + 2
  prefix#_A(x1) = 0

precedence:

  a__zWadr > a__app > app = from > mark = a__from = a__prefix > cons = s = zWadr = prefix > nil