YES
Time: 0.003305
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:
   DP:
    {f# c(X, s Y) -> f# c(s X, Y)}
   TRS:
   {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 (1):
     Scc:
      {f# c(X, s Y) -> f# c(s X, Y)}
     SCC (1):
      Strict:
       {f# c(X, s Y) -> f# c(s X, Y)}
      Weak:
      {f c(X, s Y) -> f c(s X, Y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [c](x0, x1) = x0,
        
        [f](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [f#](x0) = x0
       Strict:
        f# c(X, s Y) -> f# c(s X, Y)
        1 + 0X + 1Y >= 0 + 0X + 1Y
       Weak:
        
      Qed