YES

TRS:

  t(N) -> cs(r(q(N)),nt(ns(N)))
  q(0()) -> 0()
  q(s(X)) -> s(p(q(X),d(X)))
  d(0()) -> 0()
  d(s(X)) -> s(s(d(X)))
  p(0(),X) -> X
  p(X,0()) -> X
  p(s(X),s(Y)) -> s(s(p(X,Y)))
  f(0(),X) -> nil()
  f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z)))
  t(X) -> nt(X)
  s(X) -> ns(X)
  f(X1,X2) -> nf(X1,X2)
  a(nt(X)) -> t(a(X))
  a(ns(X)) -> s(a(X))
  a(nf(X1,X2)) -> f(a(X1),a(X2))
  a(X) -> X

linear polynomial interpretations on N:

  t_A(x1) = x1 + 4
  t#_A(x1) = 5
  cs_A(x1,x2) = x2
  cs#_A(x1,x2) = 3
  r_A(x1) = 1
  r#_A(x1) = 0
  q_A(x1) = 1
  q#_A(x1) = 4
  nt_A(x1) = x1 + 4
  nt#_A(x1) = 2
  ns_A(x1) = x1
  ns#_A(x1) = 0
  0_A = 0
  0#_A = 1
  s_A(x1) = x1
  s#_A(x1) = 1
  p_A(x1,x2) = x1 + x2
  p#_A(x1,x2) = x1 + 2
  d_A(x1) = 0
  d#_A(x1) = 2
  f_A(x1,x2) = x1 + x2 + 3
  f#_A(x1,x2) = x2 + 4
  nil_A = 0
  nil#_A = 0
  nf_A(x1,x2) = x1 + x2 + 3
  nf#_A(x1,x2) = 1
  a_A(x1) = x1
  a#_A(x1) = x1 + 2

precedence:

  nf > f > cs = ns = p > q = nt = a > t = r = 0 = s > d = nil