YES
TRS:
 {             c(X) -> d(activate(X)),
               f(X) -> n__f(X),
            f(f(X)) -> c(n__f(n__g(n__f(X)))),
               d(X) -> n__d(X),
        activate(X) -> X,
  activate(n__f(X)) -> f(activate(X)),
  activate(n__g(X)) -> g(X),
  activate(n__d(X)) -> d(X),
               h(X) -> c(n__d(X)),
               g(X) -> n__g(X)}
 RUF:
  Strict:
   {             c(X) -> d(activate(X)),
                 f(X) -> n__f(X),
              f(f(X)) -> c(n__f(n__g(n__f(X)))),
                 d(X) -> n__d(X),
          activate(X) -> X,
    activate(n__f(X)) -> f(activate(X)),
    activate(n__g(X)) -> g(X),
    activate(n__d(X)) -> d(X),
                 g(X) -> n__g(X)}
  Weak:
   {}
  DP:
   Strict:
    {             c#(X) -> d#(activate(X)),
                  c#(X) -> activate#(X),
               f#(f(X)) -> c#(n__f(n__g(n__f(X)))),
     activate#(n__f(X)) -> f#(activate(X)),
     activate#(n__f(X)) -> activate#(X),
     activate#(n__g(X)) -> g#(X),
     activate#(n__d(X)) -> d#(X)}
   Weak:
   {             c(X) -> d(activate(X)),
                 f(X) -> n__f(X),
              f(f(X)) -> c(n__f(n__g(n__f(X)))),
                 d(X) -> n__d(X),
          activate(X) -> X,
    activate(n__f(X)) -> f(activate(X)),
    activate(n__g(X)) -> g(X),
    activate(n__d(X)) -> d(X),
                 g(X) -> n__g(X)}
   EDG:
    {(activate#(n__f(X)) -> activate#(X), activate#(n__d(X)) -> d#(X))
     (activate#(n__f(X)) -> activate#(X), activate#(n__g(X)) -> g#(X))
     (activate#(n__f(X)) -> activate#(X), activate#(n__f(X)) -> activate#(X))
     (activate#(n__f(X)) -> activate#(X), activate#(n__f(X)) -> f#(activate(X)))
     (activate#(n__f(X)) -> f#(activate(X)), f#(f(X)) -> c#(n__f(n__g(n__f(X)))))
     (f#(f(X)) -> c#(n__f(n__g(n__f(X)))), c#(X) -> d#(activate(X)))
     (f#(f(X)) -> c#(n__f(n__g(n__f(X)))), c#(X) -> activate#(X))
     (c#(X) -> activate#(X), activate#(n__f(X)) -> f#(activate(X)))
     (c#(X) -> activate#(X), activate#(n__f(X)) -> activate#(X))
     (c#(X) -> activate#(X), activate#(n__g(X)) -> g#(X))
     (c#(X) -> activate#(X), activate#(n__d(X)) -> d#(X))}
    SCCS:
     Scc:
      {             c#(X) -> activate#(X),
                 f#(f(X)) -> c#(n__f(n__g(n__f(X)))),
       activate#(n__f(X)) -> f#(activate(X)),
       activate#(n__f(X)) -> activate#(X)}
     SCC:
      Strict:
       {             c#(X) -> activate#(X),
                  f#(f(X)) -> c#(n__f(n__g(n__f(X)))),
        activate#(n__f(X)) -> f#(activate(X)),
        activate#(n__f(X)) -> activate#(X)}
      Weak:
      {             c(X) -> d(activate(X)),
                    f(X) -> n__f(X),
                 f(f(X)) -> c(n__f(n__g(n__f(X)))),
                    d(X) -> n__d(X),
             activate(X) -> X,
       activate(n__f(X)) -> f(activate(X)),
       activate(n__g(X)) -> g(X),
       activate(n__d(X)) -> d(X),
                    g(X) -> n__g(X)}
      POLY:
       Argument Filtering:
        pi(g) = [], pi(n__d) = [], pi(activate#) = 0, pi(activate) = [], pi(d) = [], pi(f#) = [], pi(f) = [], pi(n__g) = [], pi(n__f) = [0], pi(c#) = 0, pi(c) = []
       Usable Rules:
        {}
       Interpretation:
        [f#] = 1,
        [n__g] = 0,
        [n__f](x0) = x0 + 1
       Strict:
        {             c#(X) -> activate#(X),
                   f#(f(X)) -> c#(n__f(n__g(n__f(X)))),
         activate#(n__f(X)) -> f#(activate(X))}
       Weak:
        {             c(X) -> d(activate(X)),
                      f(X) -> n__f(X),
                   f(f(X)) -> c(n__f(n__g(n__f(X)))),
                      d(X) -> n__d(X),
               activate(X) -> X,
         activate(n__f(X)) -> f(activate(X)),
         activate(n__g(X)) -> g(X),
         activate(n__d(X)) -> d(X),
                      g(X) -> n__g(X)}
       EDG:
        {(f#(f(X)) -> c#(n__f(n__g(n__f(X)))), c#(X) -> activate#(X))
         (activate#(n__f(X)) -> f#(activate(X)), f#(f(X)) -> c#(n__f(n__g(n__f(X)))))
         (c#(X) -> activate#(X), activate#(n__f(X)) -> f#(activate(X)))}
        SCCS:
         Scc:
          {             c#(X) -> activate#(X),
                     f#(f(X)) -> c#(n__f(n__g(n__f(X)))),
           activate#(n__f(X)) -> f#(activate(X))}
         SCC:
          Strict:
           {             c#(X) -> activate#(X),
                      f#(f(X)) -> c#(n__f(n__g(n__f(X)))),
            activate#(n__f(X)) -> f#(activate(X))}
          Weak:
          {             c(X) -> d(activate(X)),
                        f(X) -> n__f(X),
                     f(f(X)) -> c(n__f(n__g(n__f(X)))),
                        d(X) -> n__d(X),
                 activate(X) -> X,
           activate(n__f(X)) -> f(activate(X)),
           activate(n__g(X)) -> g(X),
           activate(n__d(X)) -> d(X),
                        g(X) -> n__g(X)}
          POLY:
           Argument Filtering:
            pi(g) = [], pi(n__d) = [], pi(activate#) = 0, pi(activate) = 0, pi(d) = [], pi(f#) = [0], pi(f) = [0], pi(n__g) = [], pi(n__f) = [0], pi(c#) = 0, pi(c) = [0]
           Usable Rules:
            {}
           Interpretation:
            [f#](x0) = x0 + 1,
            [f](x0) = x0 + 1,
            [n__g] = 0,
            [n__f](x0) = x0 + 1
           Strict:
            {             c#(X) -> activate#(X),
             activate#(n__f(X)) -> f#(activate(X))}
           Weak:
            {             c(X) -> d(activate(X)),
                          f(X) -> n__f(X),
                       f(f(X)) -> c(n__f(n__g(n__f(X)))),
                          d(X) -> n__d(X),
                   activate(X) -> X,
             activate(n__f(X)) -> f(activate(X)),
             activate(n__g(X)) -> g(X),
             activate(n__d(X)) -> d(X),
                          g(X) -> n__g(X)}
           EDG:
            {(c#(X) -> activate#(X), activate#(n__f(X)) -> f#(activate(X)))}
            SCCS:
             
             Qed