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