YES
TRS:
 {                 f(X) -> cons(X, n__f(n__g(X))),
                   f(X) -> n__f(X),
                   g(X) -> n__g(X),
                g(s(X)) -> s(s(g(X))),
                 g(0()) -> s(0()),
  sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)),
   sel(0(), cons(X, Y)) -> X,
            activate(X) -> X,
      activate(n__f(X)) -> f(activate(X)),
      activate(n__g(X)) -> g(activate(X))}
 DP:
  Strict:
   {              g#(s(X)) -> g#(X),
    sel#(s(X), cons(Y, Z)) -> sel#(X, activate(Z)),
    sel#(s(X), cons(Y, Z)) -> activate#(Z),
        activate#(n__f(X)) -> f#(activate(X)),
        activate#(n__f(X)) -> activate#(X),
        activate#(n__g(X)) -> g#(activate(X)),
        activate#(n__g(X)) -> activate#(X)}
  Weak:
  {                 f(X) -> cons(X, n__f(n__g(X))),
                    f(X) -> n__f(X),
                    g(X) -> n__g(X),
                 g(s(X)) -> s(s(g(X))),
                  g(0()) -> s(0()),
   sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)),
    sel(0(), cons(X, Y)) -> X,
             activate(X) -> X,
       activate(n__f(X)) -> f(activate(X)),
       activate(n__g(X)) -> g(activate(X))}
  EDG:
   {(sel#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__g(X)) -> activate#(X))
    (sel#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__g(X)) -> g#(activate(X)))
    (sel#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__f(X)) -> activate#(X))
    (sel#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__f(X)) -> f#(activate(X)))
    (activate#(n__f(X)) -> activate#(X), activate#(n__g(X)) -> activate#(X))
    (activate#(n__f(X)) -> activate#(X), activate#(n__g(X)) -> g#(activate(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__g(X)) -> g#(activate(X)), g#(s(X)) -> g#(X))
    (activate#(n__g(X)) -> activate#(X), activate#(n__f(X)) -> f#(activate(X)))
    (activate#(n__g(X)) -> activate#(X), activate#(n__f(X)) -> activate#(X))
    (activate#(n__g(X)) -> activate#(X), activate#(n__g(X)) -> g#(activate(X)))
    (activate#(n__g(X)) -> activate#(X), activate#(n__g(X)) -> activate#(X))
    (g#(s(X)) -> g#(X), g#(s(X)) -> g#(X))
    (sel#(s(X), cons(Y, Z)) -> sel#(X, activate(Z)), sel#(s(X), cons(Y, Z)) -> sel#(X, activate(Z)))
    (sel#(s(X), cons(Y, Z)) -> sel#(X, activate(Z)), sel#(s(X), cons(Y, Z)) -> activate#(Z))}
   SCCS:
    Scc:
     {activate#(n__f(X)) -> activate#(X),
      activate#(n__g(X)) -> activate#(X)}
    Scc:
     {sel#(s(X), cons(Y, Z)) -> sel#(X, activate(Z))}
    Scc:
     {g#(s(X)) -> g#(X)}
    SCC:
     Strict:
      {activate#(n__f(X)) -> activate#(X),
       activate#(n__g(X)) -> activate#(X)}
     Weak:
     {                 f(X) -> cons(X, n__f(n__g(X))),
                       f(X) -> n__f(X),
                       g(X) -> n__g(X),
                    g(s(X)) -> s(s(g(X))),
                     g(0()) -> s(0()),
      sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)),
       sel(0(), cons(X, Y)) -> X,
                activate(X) -> X,
          activate(n__f(X)) -> f(activate(X)),
          activate(n__g(X)) -> g(activate(X))}
     SPSC:
      Simple Projection:
       pi(activate#) = 0
      Strict:
       {activate#(n__g(X)) -> activate#(X)}
      EDG:
       {(activate#(n__g(X)) -> activate#(X), activate#(n__g(X)) -> activate#(X))}
       SCCS:
        Scc:
         {activate#(n__g(X)) -> activate#(X)}
        SCC:
         Strict:
          {activate#(n__g(X)) -> activate#(X)}
         Weak:
         {                 f(X) -> cons(X, n__f(n__g(X))),
                           f(X) -> n__f(X),
                           g(X) -> n__g(X),
                        g(s(X)) -> s(s(g(X))),
                         g(0()) -> s(0()),
          sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)),
           sel(0(), cons(X, Y)) -> X,
                    activate(X) -> X,
              activate(n__f(X)) -> f(activate(X)),
              activate(n__g(X)) -> g(activate(X))}
         SPSC:
          Simple Projection:
           pi(activate#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {sel#(s(X), cons(Y, Z)) -> sel#(X, activate(Z))}
     Weak:
     {                 f(X) -> cons(X, n__f(n__g(X))),
                       f(X) -> n__f(X),
                       g(X) -> n__g(X),
                    g(s(X)) -> s(s(g(X))),
                     g(0()) -> s(0()),
      sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)),
       sel(0(), cons(X, Y)) -> X,
                activate(X) -> X,
          activate(n__f(X)) -> f(activate(X)),
          activate(n__g(X)) -> g(activate(X))}
     SPSC:
      Simple Projection:
       pi(sel#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {g#(s(X)) -> g#(X)}
     Weak:
     {                 f(X) -> cons(X, n__f(n__g(X))),
                       f(X) -> n__f(X),
                       g(X) -> n__g(X),
                    g(s(X)) -> s(s(g(X))),
                     g(0()) -> s(0()),
      sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)),
       sel(0(), cons(X, Y)) -> X,
                activate(X) -> X,
          activate(n__f(X)) -> f(activate(X)),
          activate(n__g(X)) -> g(activate(X))}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {}
      Qed