YES
Time: 0.002479
TRS:
 {:(z, +(x, f y)) -> :(g(z, y), +(x, a())),
    :(:(x, y), z) -> :(x, :(y, z)),
    :(+(x, y), z) -> +(:(x, z), :(y, z))}
 DP:
  DP:
   {:#(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)}
  TRS:
  {:(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) -> :#(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))
    (:#(:(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) -> :#(x, z))
    (:#(:(x, y), z) -> :#(x, :(y, z)), :#(+(x, y), z) -> :#(y, z))}
   SCCS (1):
    Scc:
     {:#(:(x, y), z) -> :#(x, :(y, z)),
      :#(:(x, y), z) -> :#(y, z),
      :#(+(x, y), z) -> :#(x, z),
      :#(+(x, y), z) -> :#(y, z)}
    SCC (4):
     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 (1):
        Scc:
         {:#(:(x, y), z) -> :#(x, :(y, z)),
          :#(:(x, y), z) -> :#(y, z),
          :#(+(x, y), z) -> :#(y, z)}
        SCC (3):
         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 (1):
            Scc:
             {:#(:(x, y), z) -> :#(x, :(y, z)),
              :#(+(x, y), z) -> :#(y, z)}
            SCC (2):
             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 (1):
                Scc:
                 {:#(+(x, y), z) -> :#(y, z)}
                SCC (1):
                 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