YES
Time: 0.002369
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:
  DP:
   {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)}
  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}
  EDG:
   {(f#(f(x, y), z) -> f#(x, 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#(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#(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#(y, z), f#(f(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#(g(x, y), z) -> f#(y, z))
    (f#(f(x, y), z) -> f#(y, z), f#(g(x, y), z) -> f#(x, z))}
   SCCS (1):
    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 (4):
     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#(x, 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#(x, f(y, z)))
        (f#(f(x, y), z) -> f#(x, 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#(y, z), f#(f(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#(g(x, y), z) -> f#(x, z))}
       SCCS (1):
        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 (3):
         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 (1):
            Scc:
             {f#(f(x, y), z) -> f#(y, z),
              f#(g(x, y), z) -> f#(x, z)}
            SCC (2):
             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#(g(x, y), z) -> f#(x, z)}
              EDG:
               {(f#(g(x, y), z) -> f#(x, z), f#(g(x, y), z) -> f#(x, z))}
               SCCS (1):
                Scc:
                 {f#(g(x, y), z) -> f#(x, z)}
                SCC (1):
                 Strict:
                  {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:
                   {}
                  Qed