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