YES
Time: 0.056056
TRS:
 {    f 0() -> 1(),
      f s x -> g(x, s x),
  g(0(), y) -> y,
  g(s x, y) -> g(x, s +(y, x)),
  g(s x, y) -> g(x, +(y, s x)),
  +(x, 0()) -> x,
  +(x, s y) -> s +(x, y)}
 DP:
  DP:
   {    f# s x -> g#(x, s x),
    g#(s x, y) -> g#(x, s +(y, x)),
    g#(s x, y) -> g#(x, +(y, s x)),
    g#(s x, y) -> +#(y, x),
    g#(s x, y) -> +#(y, s x),
    +#(x, s y) -> +#(x, y)}
  TRS:
  {    f 0() -> 1(),
       f s x -> g(x, s x),
   g(0(), y) -> y,
   g(s x, y) -> g(x, s +(y, x)),
   g(s x, y) -> g(x, +(y, s x)),
   +(x, 0()) -> x,
   +(x, s y) -> s +(x, y)}
  UR:
   {+(x, 0()) -> x,
    +(x, s y) -> s +(x, y),
      a(z, w) -> z,
      a(z, w) -> w}
   EDG:
    {(+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (f# s x -> g#(x, s x), g#(s x, y) -> +#(y, s x))
     (f# s x -> g#(x, s x), g#(s x, y) -> +#(y, x))
     (f# s x -> g#(x, s x), g#(s x, y) -> g#(x, +(y, s x)))
     (f# s x -> g#(x, s x), g#(s x, y) -> g#(x, s +(y, x)))
     (g#(s x, y) -> g#(x, +(y, s x)), g#(s x, y) -> +#(y, s x))
     (g#(s x, y) -> g#(x, +(y, s x)), g#(s x, y) -> +#(y, x))
     (g#(s x, y) -> g#(x, +(y, s x)), g#(s x, y) -> g#(x, +(y, s x)))
     (g#(s x, y) -> g#(x, +(y, s x)), g#(s x, y) -> g#(x, s +(y, x)))
     (g#(s x, y) -> +#(y, s x), +#(x, s y) -> +#(x, y))
     (g#(s x, y) -> +#(y, x), +#(x, s y) -> +#(x, y))
     (g#(s x, y) -> g#(x, s +(y, x)), g#(s x, y) -> g#(x, s +(y, x)))
     (g#(s x, y) -> g#(x, s +(y, x)), g#(s x, y) -> g#(x, +(y, s x)))
     (g#(s x, y) -> g#(x, s +(y, x)), g#(s x, y) -> +#(y, x))
     (g#(s x, y) -> g#(x, s +(y, x)), g#(s x, y) -> +#(y, s x))}
    STATUS:
     arrows: 0.583333
     SCCS (2):
      Scc:
       {g#(s x, y) -> g#(x, s +(y, x)),
        g#(s x, y) -> g#(x, +(y, s x))}
      Scc:
       {+#(x, s y) -> +#(x, y)}
      
      
      SCC (2):
       Strict:
        {g#(s x, y) -> g#(x, s +(y, x)),
         g#(s x, y) -> g#(x, +(y, s x))}
       Weak:
       {    f 0() -> 1(),
            f s x -> g(x, s x),
        g(0(), y) -> y,
        g(s x, y) -> g(x, s +(y, x)),
        g(s x, y) -> g(x, +(y, s x)),
        +(x, 0()) -> x,
        +(x, s y) -> s +(x, y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [g](x0, x1) = 0,
         
         [+](x0, x1) = 0,
         
         [f](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [1] = 0,
         
         [0] = 1,
         
         [g#](x0, x1) = x0
        Strict:
         g#(s x, y) -> g#(x, +(y, s x))
         1 + 1x + 0y >= 0 + 1x + 0y
         g#(s x, y) -> g#(x, s +(y, x))
         1 + 1x + 0y >= 0 + 1x + 0y
        Weak:
         +(x, s y) -> s +(x, y)
         0 + 0x + 0y >= 1 + 0x + 0y
         +(x, 0()) -> x
         0 + 0x >= 1x
         g(s x, y) -> g(x, +(y, s x))
         0 + 0x + 0y >= 0 + 0x + 0y
         g(s x, y) -> g(x, s +(y, x))
         0 + 0x + 0y >= 0 + 0x + 0y
         g(0(), y) -> y
         0 + 0y >= 1y
         f s x -> g(x, s x)
         2 + 1x >= 0 + 0x
         f 0() -> 1()
         2 >= 0
       Qed
     
     
     SCC (1):
      Strict:
       {+#(x, s y) -> +#(x, y)}
      Weak:
      {    f 0() -> 1(),
           f s x -> g(x, s x),
       g(0(), y) -> y,
       g(s x, y) -> g(x, s +(y, x)),
       g(s x, y) -> g(x, +(y, s x)),
       +(x, 0()) -> x,
       +(x, s y) -> s +(x, y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [g](x0, x1) = x0 + x1 + 1,
        
        [+](x0, x1) = x0 + 1,
        
        [f](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [1] = 0,
        
        [0] = 1,
        
        [+#](x0, x1) = x0
       Strict:
        +#(x, s y) -> +#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        +(x, s y) -> s +(x, y)
        2 + 0x + 1y >= 2 + 0x + 1y
        +(x, 0()) -> x
        2 + 0x >= 1x
        g(s x, y) -> g(x, +(y, s x))
        2 + 1x + 1y >= 3 + 2x + 0y
        g(s x, y) -> g(x, s +(y, x))
        2 + 1x + 1y >= 3 + 2x + 0y
        g(0(), y) -> y
        2 + 1y >= 1y
        f s x -> g(x, s x)
        2 + 1x >= 2 + 2x
        f 0() -> 1()
        2 >= 0
      Qed