YES
Time: 0.001163
TRS:
 {      g(x, s y) -> g(f(x, y), 0()),
  g(0(), f(x, x)) -> x,
  g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0())),
        g(s x, y) -> g(f(x, y), 0())}
 RUF:
  Strict:
   {g(0(), f(x, x)) -> x,
    g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))}
  Weak:
   {}
  DP:
   DP:
    {g#(f(x, y), 0()) -> g#(x, 0()),
     g#(f(x, y), 0()) -> g#(y, 0())}
   TRS:
   {g(0(), f(x, x)) -> x,
    g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))}
   EDG:
    {(g#(f(x, y), 0()) -> g#(y, 0()), g#(f(x, y), 0()) -> g#(y, 0()))
     (g#(f(x, y), 0()) -> g#(y, 0()), g#(f(x, y), 0()) -> g#(x, 0()))
     (g#(f(x, y), 0()) -> g#(x, 0()), g#(f(x, y), 0()) -> g#(x, 0()))
     (g#(f(x, y), 0()) -> g#(x, 0()), g#(f(x, y), 0()) -> g#(y, 0()))}
    SCCS (1):
     Scc:
      {g#(f(x, y), 0()) -> g#(x, 0()),
       g#(f(x, y), 0()) -> g#(y, 0())}
     SCC (2):
      Strict:
       {g#(f(x, y), 0()) -> g#(x, 0()),
        g#(f(x, y), 0()) -> g#(y, 0())}
      Weak:
      {g(0(), f(x, x)) -> x,
       g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))}
      SPSC:
       Simple Projection:
        pi(g#) = 0
       Strict:
        {g#(f(x, y), 0()) -> g#(y, 0())}
       EDG:
        {(g#(f(x, y), 0()) -> g#(y, 0()), g#(f(x, y), 0()) -> g#(y, 0()))}
        SCCS (1):
         Scc:
          {g#(f(x, y), 0()) -> g#(y, 0())}
         SCC (1):
          Strict:
           {g#(f(x, y), 0()) -> g#(y, 0())}
          Weak:
          {g(0(), f(x, x)) -> x,
           g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))}
          SPSC:
           Simple Projection:
            pi(g#) = 0
           Strict:
            {}
           Qed