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