YES
TRS:
 {      f(x, 0()) -> x,
    f(f(x, y), z) -> f(x, f(y, z)),
        f(0(), y) -> y,
       f(i(x), y) -> i(x),
    f(g(x, y), z) -> g(f(x, z), f(y, z)),
  f(1(), g(x, y)) -> x,
  f(2(), g(x, y)) -> y}
 DP:
  Strict:
   {f#(f(x, y), z) -> f#(y, z),
    f#(f(x, y), z) -> f#(x, f(y, z)),
    f#(g(x, y), z) -> f#(y, z),
    f#(g(x, y), z) -> f#(x, z)}
  Weak:
  {      f(x, 0()) -> x,
     f(f(x, y), z) -> f(x, f(y, z)),
         f(0(), y) -> y,
        f(i(x), y) -> i(x),
     f(g(x, y), z) -> g(f(x, z), f(y, z)),
   f(1(), g(x, y)) -> x,
   f(2(), g(x, y)) -> y}
  EDG:
   {(f#(f(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(x, z))
    (f#(f(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(y, z))
    (f#(f(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(x, f(y, z)))
    (f#(f(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(y, z))
    (f#(g(x, y), z) -> f#(x, z), f#(g(x, y), z) -> f#(x, z))
    (f#(g(x, y), z) -> f#(x, z), f#(g(x, y), z) -> f#(y, z))
    (f#(g(x, y), z) -> f#(x, z), f#(f(x, y), z) -> f#(x, f(y, z)))
    (f#(g(x, y), z) -> f#(x, z), f#(f(x, y), z) -> f#(y, z))
    (f#(g(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(y, z))
    (f#(g(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(x, f(y, z)))
    (f#(g(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(y, z))
    (f#(g(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(x, z))
    (f#(f(x, y), z) -> f#(x, f(y, z)), f#(f(x, y), z) -> f#(y, z))
    (f#(f(x, y), z) -> f#(x, f(y, z)), f#(f(x, y), z) -> f#(x, f(y, z)))
    (f#(f(x, y), z) -> f#(x, f(y, z)), f#(g(x, y), z) -> f#(y, z))
    (f#(f(x, y), z) -> f#(x, f(y, z)), f#(g(x, y), z) -> f#(x, z))}
   SCCS:
    Scc:
     {f#(f(x, y), z) -> f#(y, z),
      f#(f(x, y), z) -> f#(x, f(y, z)),
      f#(g(x, y), z) -> f#(y, z),
      f#(g(x, y), z) -> f#(x, z)}
    SCC:
     Strict:
      {f#(f(x, y), z) -> f#(y, z),
       f#(f(x, y), z) -> f#(x, f(y, z)),
       f#(g(x, y), z) -> f#(y, z),
       f#(g(x, y), z) -> f#(x, z)}
     Weak:
     {      f(x, 0()) -> x,
        f(f(x, y), z) -> f(x, f(y, z)),
            f(0(), y) -> y,
           f(i(x), y) -> i(x),
        f(g(x, y), z) -> g(f(x, z), f(y, z)),
      f(1(), g(x, y)) -> x,
      f(2(), g(x, y)) -> y}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(f(x, y), z) -> f#(y, z),
        f#(f(x, y), z) -> f#(x, f(y, z)),
        f#(g(x, y), z) -> f#(x, z)}
      EDG:
       {(f#(f(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(x, z))
        (f#(f(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(x, f(y, z)))
        (f#(f(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(y, z))
        (f#(g(x, y), z) -> f#(x, z), f#(f(x, y), z) -> f#(y, z))
        (f#(g(x, y), z) -> f#(x, z), f#(f(x, y), z) -> f#(x, f(y, z)))
        (f#(g(x, y), z) -> f#(x, z), f#(g(x, y), z) -> f#(x, z))
        (f#(f(x, y), z) -> f#(x, f(y, z)), f#(f(x, y), z) -> f#(y, z))
        (f#(f(x, y), z) -> f#(x, f(y, z)), f#(f(x, y), z) -> f#(x, f(y, z)))
        (f#(f(x, y), z) -> f#(x, f(y, z)), f#(g(x, y), z) -> f#(x, z))}
       SCCS:
        Scc:
         {f#(f(x, y), z) -> f#(y, z),
          f#(f(x, y), z) -> f#(x, f(y, z)),
          f#(g(x, y), z) -> f#(x, z)}
        SCC:
         Strict:
          {f#(f(x, y), z) -> f#(y, z),
           f#(f(x, y), z) -> f#(x, f(y, z)),
           f#(g(x, y), z) -> f#(x, z)}
         Weak:
         {      f(x, 0()) -> x,
            f(f(x, y), z) -> f(x, f(y, z)),
                f(0(), y) -> y,
               f(i(x), y) -> i(x),
            f(g(x, y), z) -> g(f(x, z), f(y, z)),
          f(1(), g(x, y)) -> x,
          f(2(), g(x, y)) -> y}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {f#(f(x, y), z) -> f#(y, z),
            f#(g(x, y), z) -> f#(x, z)}
          EDG:
           {(f#(g(x, y), z) -> f#(x, z), f#(g(x, y), z) -> f#(x, z))
            (f#(g(x, y), z) -> f#(x, z), f#(f(x, y), z) -> f#(y, z))
            (f#(f(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(y, z))
            (f#(f(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(x, z))}
           SCCS:
            Scc:
             {f#(f(x, y), z) -> f#(y, z),
              f#(g(x, y), z) -> f#(x, z)}
            SCC:
             Strict:
              {f#(f(x, y), z) -> f#(y, z),
               f#(g(x, y), z) -> f#(x, z)}
             Weak:
             {      f(x, 0()) -> x,
                f(f(x, y), z) -> f(x, f(y, z)),
                    f(0(), y) -> y,
                   f(i(x), y) -> i(x),
                f(g(x, y), z) -> g(f(x, z), f(y, z)),
              f(1(), g(x, y)) -> x,
              f(2(), g(x, y)) -> y}
             SPSC:
              Simple Projection:
               pi(f#) = 0
              Strict:
               {f#(f(x, y), z) -> f#(y, z)}
              EDG:
               {(f#(f(x, y), z) -> f#(y, z), f#(f(x, y), z) -> f#(y, z))}
               SCCS:
                Scc:
                 {f#(f(x, y), z) -> f#(y, z)}
                SCC:
                 Strict:
                  {f#(f(x, y), z) -> f#(y, z)}
                 Weak:
                 {      f(x, 0()) -> x,
                    f(f(x, y), z) -> f(x, f(y, z)),
                        f(0(), y) -> y,
                       f(i(x), y) -> i(x),
                    f(g(x, y), z) -> g(f(x, z), f(y, z)),
                  f(1(), g(x, y)) -> x,
                  f(2(), g(x, y)) -> y}
                 SPSC:
                  Simple Projection:
                   pi(f#) = 0
                  Strict:
                   {}
                  Qed