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