YES
TRS:
 {   +(x, +(y, z)) -> +(+(x, y), z),
         +(x, 0()) -> x,
        +(x, s(y)) -> s(+(x, y)),
         +(0(), y) -> y,
        +(s(x), y) -> s(+(x, y)),
  f(h(x, h(y, z))) -> f(h(+(x, y), z)),
        f(g(f(x))) -> f(h(s(0()), x)),
     f(g(h(x, y))) -> f(h(s(x), y))}
 RUF:
  Strict:
   {   +(x, +(y, z)) -> +(+(x, y), z),
           +(x, 0()) -> x,
          +(x, s(y)) -> s(+(x, y)),
           +(0(), y) -> y,
          +(s(x), y) -> s(+(x, y)),
    f(h(x, h(y, z))) -> f(h(+(x, y), z))}
  Weak:
   {}
  RUF:
   Strict:
    {   +(x, +(y, z)) -> +(+(x, y), z),
           +(x, s(y)) -> s(+(x, y)),
           +(s(x), y) -> s(+(x, y)),
     f(h(x, h(y, z))) -> f(h(+(x, y), z))}
   Weak:
    {}
   DP:
    Strict:
     {   +#(x, +(y, z)) -> +#(x, y),
         +#(x, +(y, z)) -> +#(+(x, y), z),
            +#(x, s(y)) -> +#(x, y),
            +#(s(x), y) -> +#(x, y),
      f#(h(x, h(y, z))) -> +#(x, y),
      f#(h(x, h(y, z))) -> f#(h(+(x, y), z))}
    Weak:
    {   +(x, +(y, z)) -> +(+(x, y), z),
           +(x, s(y)) -> s(+(x, y)),
           +(s(x), y) -> s(+(x, y)),
     f(h(x, h(y, z))) -> f(h(+(x, y), z))}
    EDG:
     {(+#(x, s(y)) -> +#(x, y), +#(s(x), y) -> +#(x, y))
      (+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
      (+#(x, s(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
      (+#(x, s(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
      (f#(h(x, h(y, z))) -> +#(x, y), +#(s(x), y) -> +#(x, y))
      (f#(h(x, h(y, z))) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
      (f#(h(x, h(y, z))) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
      (f#(h(x, h(y, z))) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
      (f#(h(x, h(y, z))) -> f#(h(+(x, y), z)), f#(h(x, h(y, z))) -> f#(h(+(x, y), z)))
      (f#(h(x, h(y, z))) -> f#(h(+(x, y), z)), f#(h(x, h(y, z))) -> +#(x, y))
      (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y))
      (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
      (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, s(y)) -> +#(x, y))
      (+#(x, +(y, z)) -> +#(+(x, y), z), +#(s(x), y) -> +#(x, y))
      (+#(s(x), y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
      (+#(s(x), y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
      (+#(s(x), y) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
      (+#(s(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y))
      (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
      (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
      (+#(x, +(y, z)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
      (+#(x, +(y, z)) -> +#(x, y), +#(s(x), y) -> +#(x, y))}
     SCCS:
      Scc:
       {f#(h(x, h(y, z))) -> f#(h(+(x, y), z))}
      Scc:
       {+#(x, +(y, z)) -> +#(x, y),
        +#(x, +(y, z)) -> +#(+(x, y), z),
           +#(x, s(y)) -> +#(x, y),
           +#(s(x), y) -> +#(x, y)}
      SCC:
       Strict:
        {f#(h(x, h(y, z))) -> f#(h(+(x, y), z))}
       Weak:
       {   +(x, +(y, z)) -> +(+(x, y), z),
              +(x, s(y)) -> s(+(x, y)),
              +(s(x), y) -> s(+(x, y)),
        f(h(x, h(y, z))) -> f(h(+(x, y), z))}
       POLY:
        Argument Filtering:
         pi(h) = [1], pi(f#) = 0, pi(f) = [], pi(s) = [], pi(+) = []
        Usable Rules:
         {}
        Interpretation:
         [h](x0) = x0 + 1
        Strict:
         {}
        Weak:
         {   +(x, +(y, z)) -> +(+(x, y), z),
                +(x, s(y)) -> s(+(x, y)),
                +(s(x), y) -> s(+(x, y)),
          f(h(x, h(y, z))) -> f(h(+(x, y), z))}
        Qed
      SCC:
       Strict:
        {+#(x, +(y, z)) -> +#(x, y),
         +#(x, +(y, z)) -> +#(+(x, y), z),
            +#(x, s(y)) -> +#(x, y),
            +#(s(x), y) -> +#(x, y)}
       Weak:
       {   +(x, +(y, z)) -> +(+(x, y), z),
              +(x, s(y)) -> s(+(x, y)),
              +(s(x), y) -> s(+(x, y)),
        f(h(x, h(y, z))) -> f(h(+(x, y), z))}
       SPSC:
        Simple Projection:
         pi(+#) = 1
        Strict:
         {+#(x, +(y, z)) -> +#(x, y),
          +#(x, +(y, z)) -> +#(+(x, y), z),
             +#(s(x), y) -> +#(x, y)}
        EDG:
         {(+#(x, +(y, z)) -> +#(x, y), +#(s(x), y) -> +#(x, y))
          (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
          (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
          (+#(s(x), y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
          (+#(s(x), y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
          (+#(s(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y))
          (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y))
          (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
          (+#(x, +(y, z)) -> +#(+(x, y), z), +#(s(x), y) -> +#(x, y))}
         SCCS:
          Scc:
           {+#(x, +(y, z)) -> +#(x, y),
            +#(x, +(y, z)) -> +#(+(x, y), z),
               +#(s(x), y) -> +#(x, y)}
          SCC:
           Strict:
            {+#(x, +(y, z)) -> +#(x, y),
             +#(x, +(y, z)) -> +#(+(x, y), z),
                +#(s(x), y) -> +#(x, y)}
           Weak:
           {   +(x, +(y, z)) -> +(+(x, y), z),
                  +(x, s(y)) -> s(+(x, y)),
                  +(s(x), y) -> s(+(x, y)),
            f(h(x, h(y, z))) -> f(h(+(x, y), z))}
           SPSC:
            Simple Projection:
             pi(+#) = 1
            Strict:
             {+#(x, +(y, z)) -> +#(x, y),
                 +#(s(x), y) -> +#(x, y)}
            EDG:
             {(+#(s(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y))
              (+#(s(x), y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
              (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
              (+#(x, +(y, z)) -> +#(x, y), +#(s(x), y) -> +#(x, y))}
             SCCS:
              Scc:
               {+#(x, +(y, z)) -> +#(x, y),
                   +#(s(x), y) -> +#(x, y)}
              SCC:
               Strict:
                {+#(x, +(y, z)) -> +#(x, y),
                    +#(s(x), y) -> +#(x, y)}
               Weak:
               {   +(x, +(y, z)) -> +(+(x, y), z),
                      +(x, s(y)) -> s(+(x, y)),
                      +(s(x), y) -> s(+(x, y)),
                f(h(x, h(y, z))) -> f(h(+(x, y), z))}
               SPSC:
                Simple Projection:
                 pi(+#) = 0
                Strict:
                 {+#(x, +(y, z)) -> +#(x, y)}
                EDG:
                 {(+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))}
                 SCCS:
                  Scc:
                   {+#(x, +(y, z)) -> +#(x, y)}
                  SCC:
                   Strict:
                    {+#(x, +(y, z)) -> +#(x, y)}
                   Weak:
                   {   +(x, +(y, z)) -> +(+(x, y), z),
                          +(x, s(y)) -> s(+(x, y)),
                          +(s(x), y) -> s(+(x, y)),
                    f(h(x, h(y, z))) -> f(h(+(x, y), z))}
                   SPSC:
                    Simple Projection:
                     pi(+#) = 1
                    Strict:
                     {}
                    Qed