YES
TRS:
 {           q(0()) -> 0(),
            q(s(X)) -> s(p(q(X), d(X))),
               t(N) -> cs(r(q(N)), nt(ns(N))),
               t(X) -> nt(X),
               s(X) -> ns(X),
          p(X, 0()) -> X,
          p(0(), X) -> X,
      p(s(X), s(Y)) -> s(s(p(X, Y))),
             d(0()) -> 0(),
            d(s(X)) -> s(s(d(X))),
          f(X1, X2) -> nf(X1, X2),
          f(0(), X) -> nil(),
  f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
               a(X) -> X,
           a(nt(X)) -> t(a(X)),
           a(ns(X)) -> s(a(X)),
      a(nf(X1, X2)) -> f(a(X1), a(X2))}
 DP:
  Strict:
   {          q#(s(X)) -> q#(X),
              q#(s(X)) -> s#(p(q(X), d(X))),
              q#(s(X)) -> p#(q(X), d(X)),
              q#(s(X)) -> d#(X),
                 t#(N) -> q#(N),
        p#(s(X), s(Y)) -> s#(s(p(X, Y))),
        p#(s(X), s(Y)) -> s#(p(X, Y)),
        p#(s(X), s(Y)) -> p#(X, Y),
              d#(s(X)) -> s#(s(d(X))),
              d#(s(X)) -> s#(d(X)),
              d#(s(X)) -> d#(X),
    f#(s(X), cs(Y, Z)) -> a#(Z),
             a#(nt(X)) -> t#(a(X)),
             a#(nt(X)) -> a#(X),
             a#(ns(X)) -> s#(a(X)),
             a#(ns(X)) -> a#(X),
        a#(nf(X1, X2)) -> f#(a(X1), a(X2)),
        a#(nf(X1, X2)) -> a#(X1),
        a#(nf(X1, X2)) -> a#(X2)}
  Weak:
  {           q(0()) -> 0(),
             q(s(X)) -> s(p(q(X), d(X))),
                t(N) -> cs(r(q(N)), nt(ns(N))),
                t(X) -> nt(X),
                s(X) -> ns(X),
           p(X, 0()) -> X,
           p(0(), X) -> X,
       p(s(X), s(Y)) -> s(s(p(X, Y))),
              d(0()) -> 0(),
             d(s(X)) -> s(s(d(X))),
           f(X1, X2) -> nf(X1, X2),
           f(0(), X) -> nil(),
   f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                a(X) -> X,
            a(nt(X)) -> t(a(X)),
            a(ns(X)) -> s(a(X)),
       a(nf(X1, X2)) -> f(a(X1), a(X2))}
  EDG:
   {(q#(s(X)) -> q#(X), q#(s(X)) -> d#(X))
    (q#(s(X)) -> q#(X), q#(s(X)) -> p#(q(X), d(X)))
    (q#(s(X)) -> q#(X), q#(s(X)) -> s#(p(q(X), d(X))))
    (q#(s(X)) -> q#(X), q#(s(X)) -> q#(X))
    (d#(s(X)) -> d#(X), d#(s(X)) -> d#(X))
    (d#(s(X)) -> d#(X), d#(s(X)) -> s#(d(X)))
    (d#(s(X)) -> d#(X), d#(s(X)) -> s#(s(d(X))))
    (a#(nt(X)) -> a#(X), a#(nf(X1, X2)) -> a#(X2))
    (a#(nt(X)) -> a#(X), a#(nf(X1, X2)) -> a#(X1))
    (a#(nt(X)) -> a#(X), a#(nf(X1, X2)) -> f#(a(X1), a(X2)))
    (a#(nt(X)) -> a#(X), a#(ns(X)) -> a#(X))
    (a#(nt(X)) -> a#(X), a#(ns(X)) -> s#(a(X)))
    (a#(nt(X)) -> a#(X), a#(nt(X)) -> a#(X))
    (a#(nt(X)) -> a#(X), a#(nt(X)) -> t#(a(X)))
    (a#(nf(X1, X2)) -> a#(X2), a#(nf(X1, X2)) -> a#(X2))
    (a#(nf(X1, X2)) -> a#(X2), a#(nf(X1, X2)) -> a#(X1))
    (a#(nf(X1, X2)) -> a#(X2), a#(nf(X1, X2)) -> f#(a(X1), a(X2)))
    (a#(nf(X1, X2)) -> a#(X2), a#(ns(X)) -> a#(X))
    (a#(nf(X1, X2)) -> a#(X2), a#(ns(X)) -> s#(a(X)))
    (a#(nf(X1, X2)) -> a#(X2), a#(nt(X)) -> a#(X))
    (a#(nf(X1, X2)) -> a#(X2), a#(nt(X)) -> t#(a(X)))
    (a#(nt(X)) -> t#(a(X)), t#(N) -> q#(N))
    (p#(s(X), s(Y)) -> p#(X, Y), p#(s(X), s(Y)) -> p#(X, Y))
    (p#(s(X), s(Y)) -> p#(X, Y), p#(s(X), s(Y)) -> s#(p(X, Y)))
    (p#(s(X), s(Y)) -> p#(X, Y), p#(s(X), s(Y)) -> s#(s(p(X, Y))))
    (t#(N) -> q#(N), q#(s(X)) -> d#(X))
    (t#(N) -> q#(N), q#(s(X)) -> p#(q(X), d(X)))
    (t#(N) -> q#(N), q#(s(X)) -> s#(p(q(X), d(X))))
    (t#(N) -> q#(N), q#(s(X)) -> q#(X))
    (a#(nf(X1, X2)) -> a#(X1), a#(nt(X)) -> t#(a(X)))
    (a#(nf(X1, X2)) -> a#(X1), a#(nt(X)) -> a#(X))
    (a#(nf(X1, X2)) -> a#(X1), a#(ns(X)) -> s#(a(X)))
    (a#(nf(X1, X2)) -> a#(X1), a#(ns(X)) -> a#(X))
    (a#(nf(X1, X2)) -> a#(X1), a#(nf(X1, X2)) -> f#(a(X1), a(X2)))
    (a#(nf(X1, X2)) -> a#(X1), a#(nf(X1, X2)) -> a#(X1))
    (a#(nf(X1, X2)) -> a#(X1), a#(nf(X1, X2)) -> a#(X2))
    (a#(ns(X)) -> a#(X), a#(nt(X)) -> t#(a(X)))
    (a#(ns(X)) -> a#(X), a#(nt(X)) -> a#(X))
    (a#(ns(X)) -> a#(X), a#(ns(X)) -> s#(a(X)))
    (a#(ns(X)) -> a#(X), a#(ns(X)) -> a#(X))
    (a#(ns(X)) -> a#(X), a#(nf(X1, X2)) -> f#(a(X1), a(X2)))
    (a#(ns(X)) -> a#(X), a#(nf(X1, X2)) -> a#(X1))
    (a#(ns(X)) -> a#(X), a#(nf(X1, X2)) -> a#(X2))
    (f#(s(X), cs(Y, Z)) -> a#(Z), a#(nt(X)) -> t#(a(X)))
    (f#(s(X), cs(Y, Z)) -> a#(Z), a#(nt(X)) -> a#(X))
    (f#(s(X), cs(Y, Z)) -> a#(Z), a#(ns(X)) -> s#(a(X)))
    (f#(s(X), cs(Y, Z)) -> a#(Z), a#(ns(X)) -> a#(X))
    (f#(s(X), cs(Y, Z)) -> a#(Z), a#(nf(X1, X2)) -> f#(a(X1), a(X2)))
    (f#(s(X), cs(Y, Z)) -> a#(Z), a#(nf(X1, X2)) -> a#(X1))
    (f#(s(X), cs(Y, Z)) -> a#(Z), a#(nf(X1, X2)) -> a#(X2))
    (q#(s(X)) -> d#(X), d#(s(X)) -> s#(s(d(X))))
    (q#(s(X)) -> d#(X), d#(s(X)) -> s#(d(X)))
    (q#(s(X)) -> d#(X), d#(s(X)) -> d#(X))
    (a#(nf(X1, X2)) -> f#(a(X1), a(X2)), f#(s(X), cs(Y, Z)) -> a#(Z))
    (q#(s(X)) -> p#(q(X), d(X)), p#(s(X), s(Y)) -> s#(s(p(X, Y))))
    (q#(s(X)) -> p#(q(X), d(X)), p#(s(X), s(Y)) -> s#(p(X, Y)))
    (q#(s(X)) -> p#(q(X), d(X)), p#(s(X), s(Y)) -> p#(X, Y))}
   SCCS:
    Scc:
     {f#(s(X), cs(Y, Z)) -> a#(Z),
               a#(nt(X)) -> a#(X),
               a#(ns(X)) -> a#(X),
          a#(nf(X1, X2)) -> f#(a(X1), a(X2)),
          a#(nf(X1, X2)) -> a#(X1),
          a#(nf(X1, X2)) -> a#(X2)}
    Scc:
     {d#(s(X)) -> d#(X)}
    Scc:
     {p#(s(X), s(Y)) -> p#(X, Y)}
    Scc:
     {q#(s(X)) -> q#(X)}
    SCC:
     Strict:
      {f#(s(X), cs(Y, Z)) -> a#(Z),
                a#(nt(X)) -> a#(X),
                a#(ns(X)) -> a#(X),
           a#(nf(X1, X2)) -> f#(a(X1), a(X2)),
           a#(nf(X1, X2)) -> a#(X1),
           a#(nf(X1, X2)) -> a#(X2)}
     Weak:
     {           q(0()) -> 0(),
                q(s(X)) -> s(p(q(X), d(X))),
                   t(N) -> cs(r(q(N)), nt(ns(N))),
                   t(X) -> nt(X),
                   s(X) -> ns(X),
              p(X, 0()) -> X,
              p(0(), X) -> X,
          p(s(X), s(Y)) -> s(s(p(X, Y))),
                 d(0()) -> 0(),
                d(s(X)) -> s(s(d(X))),
              f(X1, X2) -> nf(X1, X2),
              f(0(), X) -> nil(),
      f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                   a(X) -> X,
               a(nt(X)) -> t(a(X)),
               a(ns(X)) -> s(a(X)),
          a(nf(X1, X2)) -> f(a(X1), a(X2))}
     POLY:
      Argument Filtering:
       pi(a#) = 0, pi(a) = 0, pi(nf) = [0,1], pi(f#) = 1, pi(f) = [0,1], pi(nil) = [], pi(d) = [], pi(p) = [], pi(s) = 0, pi(0) = [], pi(t) = 0, pi(ns) = 0, pi(nt) = 0, pi(q) = [], pi(r) = [], pi(cs) = 1
      Usable Rules:
       {}
      Interpretation:
       [nf](x0, x1) = x0 + x1 + 1
      Strict:
       {f#(s(X), cs(Y, Z)) -> a#(Z),
                 a#(nt(X)) -> a#(X),
                 a#(ns(X)) -> a#(X)}
      Weak:
       {           q(0()) -> 0(),
                  q(s(X)) -> s(p(q(X), d(X))),
                     t(N) -> cs(r(q(N)), nt(ns(N))),
                     t(X) -> nt(X),
                     s(X) -> ns(X),
                p(X, 0()) -> X,
                p(0(), X) -> X,
            p(s(X), s(Y)) -> s(s(p(X, Y))),
                   d(0()) -> 0(),
                  d(s(X)) -> s(s(d(X))),
                f(X1, X2) -> nf(X1, X2),
                f(0(), X) -> nil(),
        f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                     a(X) -> X,
                 a(nt(X)) -> t(a(X)),
                 a(ns(X)) -> s(a(X)),
            a(nf(X1, X2)) -> f(a(X1), a(X2))}
      EDG:
       {(a#(nt(X)) -> a#(X), a#(ns(X)) -> a#(X))
        (a#(nt(X)) -> a#(X), a#(nt(X)) -> a#(X))
        (a#(ns(X)) -> a#(X), a#(nt(X)) -> a#(X))
        (a#(ns(X)) -> a#(X), a#(ns(X)) -> a#(X))
        (f#(s(X), cs(Y, Z)) -> a#(Z), a#(nt(X)) -> a#(X))
        (f#(s(X), cs(Y, Z)) -> a#(Z), a#(ns(X)) -> a#(X))}
       SCCS:
        Scc:
         {a#(nt(X)) -> a#(X),
          a#(ns(X)) -> a#(X)}
        SCC:
         Strict:
          {a#(nt(X)) -> a#(X),
           a#(ns(X)) -> a#(X)}
         Weak:
         {           q(0()) -> 0(),
                    q(s(X)) -> s(p(q(X), d(X))),
                       t(N) -> cs(r(q(N)), nt(ns(N))),
                       t(X) -> nt(X),
                       s(X) -> ns(X),
                  p(X, 0()) -> X,
                  p(0(), X) -> X,
              p(s(X), s(Y)) -> s(s(p(X, Y))),
                     d(0()) -> 0(),
                    d(s(X)) -> s(s(d(X))),
                  f(X1, X2) -> nf(X1, X2),
                  f(0(), X) -> nil(),
          f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                       a(X) -> X,
                   a(nt(X)) -> t(a(X)),
                   a(ns(X)) -> s(a(X)),
              a(nf(X1, X2)) -> f(a(X1), a(X2))}
         SPSC:
          Simple Projection:
           pi(a#) = 0
          Strict:
           {a#(ns(X)) -> a#(X)}
          EDG:
           {(a#(ns(X)) -> a#(X), a#(ns(X)) -> a#(X))}
           SCCS:
            Scc:
             {a#(ns(X)) -> a#(X)}
            SCC:
             Strict:
              {a#(ns(X)) -> a#(X)}
             Weak:
             {           q(0()) -> 0(),
                        q(s(X)) -> s(p(q(X), d(X))),
                           t(N) -> cs(r(q(N)), nt(ns(N))),
                           t(X) -> nt(X),
                           s(X) -> ns(X),
                      p(X, 0()) -> X,
                      p(0(), X) -> X,
                  p(s(X), s(Y)) -> s(s(p(X, Y))),
                         d(0()) -> 0(),
                        d(s(X)) -> s(s(d(X))),
                      f(X1, X2) -> nf(X1, X2),
                      f(0(), X) -> nil(),
              f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                           a(X) -> X,
                       a(nt(X)) -> t(a(X)),
                       a(ns(X)) -> s(a(X)),
                  a(nf(X1, X2)) -> f(a(X1), a(X2))}
             SPSC:
              Simple Projection:
               pi(a#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {d#(s(X)) -> d#(X)}
     Weak:
     {           q(0()) -> 0(),
                q(s(X)) -> s(p(q(X), d(X))),
                   t(N) -> cs(r(q(N)), nt(ns(N))),
                   t(X) -> nt(X),
                   s(X) -> ns(X),
              p(X, 0()) -> X,
              p(0(), X) -> X,
          p(s(X), s(Y)) -> s(s(p(X, Y))),
                 d(0()) -> 0(),
                d(s(X)) -> s(s(d(X))),
              f(X1, X2) -> nf(X1, X2),
              f(0(), X) -> nil(),
      f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                   a(X) -> X,
               a(nt(X)) -> t(a(X)),
               a(ns(X)) -> s(a(X)),
          a(nf(X1, X2)) -> f(a(X1), a(X2))}
     SPSC:
      Simple Projection:
       pi(d#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {p#(s(X), s(Y)) -> p#(X, Y)}
     Weak:
     {           q(0()) -> 0(),
                q(s(X)) -> s(p(q(X), d(X))),
                   t(N) -> cs(r(q(N)), nt(ns(N))),
                   t(X) -> nt(X),
                   s(X) -> ns(X),
              p(X, 0()) -> X,
              p(0(), X) -> X,
          p(s(X), s(Y)) -> s(s(p(X, Y))),
                 d(0()) -> 0(),
                d(s(X)) -> s(s(d(X))),
              f(X1, X2) -> nf(X1, X2),
              f(0(), X) -> nil(),
      f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                   a(X) -> X,
               a(nt(X)) -> t(a(X)),
               a(ns(X)) -> s(a(X)),
          a(nf(X1, X2)) -> f(a(X1), a(X2))}
     SPSC:
      Simple Projection:
       pi(p#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {q#(s(X)) -> q#(X)}
     Weak:
     {           q(0()) -> 0(),
                q(s(X)) -> s(p(q(X), d(X))),
                   t(N) -> cs(r(q(N)), nt(ns(N))),
                   t(X) -> nt(X),
                   s(X) -> ns(X),
              p(X, 0()) -> X,
              p(0(), X) -> X,
          p(s(X), s(Y)) -> s(s(p(X, Y))),
                 d(0()) -> 0(),
                d(s(X)) -> s(s(d(X))),
              f(X1, X2) -> nf(X1, X2),
              f(0(), X) -> nil(),
      f(s(X), cs(Y, Z)) -> cs(Y, nf(X, a(Z))),
                   a(X) -> X,
               a(nt(X)) -> t(a(X)),
               a(ns(X)) -> s(a(X)),
          a(nf(X1, X2)) -> f(a(X1), a(X2))}
     SPSC:
      Simple Projection:
       pi(q#) = 0
      Strict:
       {}
      Qed