YES
Time: 0.014037
TRS:
 {f c(s x, y) -> f c(x, s y),
  g c(x, s y) -> g c(s x, y)}
 DP:
  DP:
   {f# c(s x, y) -> f# c(x, s y),
    g# c(x, s y) -> g# c(s x, y)}
  TRS:
  {f c(s x, y) -> f c(x, s y),
   g c(x, s y) -> g c(s x, y)}
  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))}
   STATUS:
    arrows: 0.500000
    SCCS (2):
     Scc:
      {g# c(x, s y) -> g# c(s x, y)}
     Scc:
      {f# c(s x, y) -> f# c(x, s y)}
     
     SCC (1):
      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)}
      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,
        
        [g](x0) = 0,
        
        [g#](x0) = x0
       Strict:
        g# c(x, s y) -> g# c(s x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        g c(x, s y) -> g c(s x, y)
        0 + 0x + 0y >= 0 + 0x + 0y
        f c(s x, y) -> f c(x, s y)
        0 + 0x + 0y >= 0 + 0x + 0y
      Qed
    SCC (1):
     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)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [c](x0, x1) = x0,
       
       [f](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [g](x0) = 0,
       
       [f#](x0) = x0
      Strict:
       f# c(s x, y) -> f# c(x, s y)
       1 + 1x + 0y >= 0 + 1x + 0y
      Weak:
       g c(x, s y) -> g c(s x, y)
       0 + 0x + 0y >= 0 + 0x + 0y
       f c(s x, y) -> f c(x, s y)
       2 + 1x + 0y >= 1 + 1x + 0y
     Qed