YES
TRS:
 {f(c(s(x), y)) -> f(c(x, s(y))),
  g(c(x, s(y))) -> g(c(s(x), y)),
     g(s(f(x))) -> g(f(x))}
 DP:
  Strict:
   {f#(c(s(x), y)) -> f#(c(x, s(y))),
    g#(c(x, s(y))) -> g#(c(s(x), y)),
       g#(s(f(x))) -> g#(f(x))}
  Weak:
  {f(c(s(x), y)) -> f(c(x, s(y))),
   g(c(x, s(y))) -> g(c(s(x), y)),
      g(s(f(x))) -> g(f(x))}
  EDG:
   {(g#(c(x, s(y))) -> g#(c(s(x), y)), g#(c(x, s(y))) -> g#(c(s(x), y)))
    (f#(c(s(x), y)) -> f#(c(x, s(y))), f#(c(s(x), y)) -> f#(c(x, s(y))))}
   SCCS:
    Scc:
     {g#(c(x, s(y))) -> g#(c(s(x), y))}
    Scc:
     {f#(c(s(x), y)) -> f#(c(x, s(y)))}
    SCC:
     Strict:
      {g#(c(x, s(y))) -> g#(c(s(x), y))}
     Weak:
     {f(c(s(x), y)) -> f(c(x, s(y))),
      g(c(x, s(y))) -> g(c(s(x), y)),
         g(s(f(x))) -> g(f(x))}
     POLY:
      Argument Filtering:
       pi(g#) = 0, pi(g) = [], pi(s) = [0], pi(c) = 1, pi(f) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {f(c(s(x), y)) -> f(c(x, s(y))),
        g(c(x, s(y))) -> g(c(s(x), y)),
           g(s(f(x))) -> g(f(x))}
      Qed
    SCC:
     Strict:
      {f#(c(s(x), y)) -> f#(c(x, s(y)))}
     Weak:
     {f(c(s(x), y)) -> f(c(x, s(y))),
      g(c(x, s(y))) -> g(c(s(x), y)),
         g(s(f(x))) -> g(f(x))}
     POLY:
      Argument Filtering:
       pi(g) = [], pi(s) = [0], pi(c) = 0, pi(f#) = 0, pi(f) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {f(c(s(x), y)) -> f(c(x, s(y))),
        g(c(x, s(y))) -> g(c(s(x), y)),
           g(s(f(x))) -> g(f(x))}
      Qed