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