YES

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

Proof:
 DP Processor:
  DPs:
   t#(N) -> q#(N)
   q#(s(X)) -> d#(X)
   q#(s(X)) -> q#(X)
   q#(s(X)) -> p#(q(X),d(X))
   q#(s(X)) -> s#(p(q(X),d(X)))
   d#(s(X)) -> d#(X)
   d#(s(X)) -> s#(d(X))
   d#(s(X)) -> s#(s(d(X)))
   p#(s(X),s(Y)) -> p#(X,Y)
   p#(s(X),s(Y)) -> s#(p(X,Y))
   p#(s(X),s(Y)) -> s#(s(p(X,Y)))
   f#(s(X),cs(Y,Z)) -> a#(Z)
   a#(nt(X)) -> a#(X)
   a#(nt(X)) -> t#(a(X))
   a#(ns(X)) -> a#(X)
   a#(ns(X)) -> s#(a(X))
   a#(nf(X1,X2)) -> a#(X2)
   a#(nf(X1,X2)) -> a#(X1)
   a#(nf(X1,X2)) -> f#(a(X1),a(X2))
  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
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    t(N) -> cs(r(q(N)),nt(ns(N)))
    d(0()) -> 0()
    d(s(X)) -> s(s(d(X)))
    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
   interpretation:
    [a#](x0) = x0 + 3,
    
    [f#](x0, x1) = 2x1 + 7/2,
    
    [s#](x0) = 0,
    
    [p#](x0, x1) = x1,
    
    [d#](x0) = x0,
    
    [q#](x0) = 2x0 + 3,
    
    [t#](x0) = 2x0 + 7/2,
    
    [nf](x0, x1) = x0 + 2x1 + 2,
    
    [a](x0) = x0,
    
    [nil] = 3,
    
    [f](x0, x1) = x0 + 2x1 + 2,
    
    [p](x0, x1) = x0 + x1 + 2,
    
    [d](x0) = 2x0,
    
    [s](x0) = x0 + 1/2,
    
    [0] = 1,
    
    [cs](x0, x1) = 1/2x1,
    
    [nt](x0) = 2x0 + 1,
    
    [ns](x0) = x0 + 1/2,
    
    [r](x0) = 0,
    
    [q](x0) = 2x0 + 5/2,
    
    [t](x0) = 2x0 + 1
   orientation:
    t#(N) = 2N + 7/2 >= 2N + 3 = q#(N)
    
    q#(s(X)) = 2X + 4 >= X = d#(X)
    
    q#(s(X)) = 2X + 4 >= 2X + 3 = q#(X)
    
    q#(s(X)) = 2X + 4 >= 2X = p#(q(X),d(X))
    
    q#(s(X)) = 2X + 4 >= 0 = s#(p(q(X),d(X)))
    
    d#(s(X)) = X + 1/2 >= X = d#(X)
    
    d#(s(X)) = X + 1/2 >= 0 = s#(d(X))
    
    d#(s(X)) = X + 1/2 >= 0 = s#(s(d(X)))
    
    p#(s(X),s(Y)) = Y + 1/2 >= Y = p#(X,Y)
    
    p#(s(X),s(Y)) = Y + 1/2 >= 0 = s#(p(X,Y))
    
    p#(s(X),s(Y)) = Y + 1/2 >= 0 = s#(s(p(X,Y)))
    
    f#(s(X),cs(Y,Z)) = Z + 7/2 >= Z + 3 = a#(Z)
    
    a#(nt(X)) = 2X + 4 >= X + 3 = a#(X)
    
    a#(nt(X)) = 2X + 4 >= 2X + 7/2 = t#(a(X))
    
    a#(ns(X)) = X + 7/2 >= X + 3 = a#(X)
    
    a#(ns(X)) = X + 7/2 >= 0 = s#(a(X))
    
    a#(nf(X1,X2)) = X1 + 2X2 + 5 >= X2 + 3 = a#(X2)
    
    a#(nf(X1,X2)) = X1 + 2X2 + 5 >= X1 + 3 = a#(X1)
    
    a#(nf(X1,X2)) = X1 + 2X2 + 5 >= 2X2 + 7/2 = f#(a(X1),a(X2))
    
    t(N) = 2N + 1 >= N + 1 = cs(r(q(N)),nt(ns(N)))
    
    q(0()) = 9/2 >= 1 = 0()
    
    q(s(X)) = 2X + 7/2 >= 4X + 5 = s(p(q(X),d(X)))
    
    d(0()) = 2 >= 1 = 0()
    
    d(s(X)) = 2X + 1 >= 2X + 1 = s(s(d(X)))
    
    p(0(),X) = X + 3 >= X = X
    
    p(X,0()) = X + 3 >= X = X
    
    p(s(X),s(Y)) = X + Y + 3 >= X + Y + 3 = s(s(p(X,Y)))
    
    f(0(),X) = 2X + 3 >= 3 = nil()
    
    f(s(X),cs(Y,Z)) = X + Z + 5/2 >= 1/2X + Z + 1 = cs(Y,nf(X,a(Z)))
    
    t(X) = 2X + 1 >= 2X + 1 = nt(X)
    
    s(X) = X + 1/2 >= X + 1/2 = ns(X)
    
    f(X1,X2) = X1 + 2X2 + 2 >= X1 + 2X2 + 2 = nf(X1,X2)
    
    a(nt(X)) = 2X + 1 >= 2X + 1 = t(a(X))
    
    a(ns(X)) = X + 1/2 >= X + 1/2 = s(a(X))
    
    a(nf(X1,X2)) = X1 + 2X2 + 2 >= X1 + 2X2 + 2 = f(a(X1),a(X2))
    
    a(X) = X >= X = X
   problem:
    DPs:
     
    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
   Qed