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