YES
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:
  Strict:
   {   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)}
  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))}
  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)))}
   SCCS:
    Scc:
     {+#(x, s(y)) -> +#(x, y)}
    Scc:
     {g#(s(x), y) -> g#(x, s(+(y, x))),
      g#(s(x), y) -> g#(x, +(y, s(x)))}
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(+#) = 1
      Strict:
       {}
      Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {g#(s(x), y) -> g#(x, +(y, s(x)))}
      EDG:
       {(g#(s(x), y) -> g#(x, +(y, s(x))), g#(s(x), y) -> g#(x, +(y, s(x))))}
       SCCS:
        Scc:
         {g#(s(x), y) -> g#(x, +(y, s(x)))}
        SCC:
         Strict:
          {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))}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {}
          Qed