YES
TRS:
 {f(f(x, a()), y) -> f(y, f(x, y))}
 DP:
  Strict:
   {f#(f(x, a()), y) -> f#(y, f(x, y)),
    f#(f(x, a()), y) -> f#(x, y)}
  Weak:
  {f(f(x, a()), y) -> f(y, f(x, y))}
  EDG:
   {(f#(f(x, a()), y) -> f#(y, f(x, y)), f#(f(x, a()), y) -> f#(x, y))
    (f#(f(x, a()), y) -> f#(y, f(x, y)), f#(f(x, a()), y) -> f#(y, f(x, y)))
    (f#(f(x, a()), y) -> f#(x, y), f#(f(x, a()), y) -> f#(y, f(x, y)))
    (f#(f(x, a()), y) -> f#(x, y), f#(f(x, a()), y) -> f#(x, y))}
   SCCS:
    Scc:
     {f#(f(x, a()), y) -> f#(y, f(x, y)),
      f#(f(x, a()), y) -> f#(x, y)}
    SCC:
     Strict:
      {f#(f(x, a()), y) -> f#(y, f(x, y)),
       f#(f(x, a()), y) -> f#(x, y)}
     Weak:
     {f(f(x, a()), y) -> f(y, f(x, y))}
     UR:
      {f(f(x, a()), y) -> f(y, f(x, y)),
               b(z, w) -> z,
               b(z, w) -> w}
      BOUND:
       Bound: top(-raise)-DP-bounded by 2
       Automaton:
        { b_0(10, 10) -> 8*
           b_0(10, 9) -> 8*
           b_0(10, 8) -> 8*
           b_0(9, 10) -> 8*
            b_0(9, 9) -> 8*
            b_0(9, 8) -> 8*
           b_0(8, 10) -> 8*
            b_0(8, 9) -> 8*
            b_0(8, 8) -> 8*
                a_0() -> 9*
         f#_2(11, 12) -> 5*
         f#_1(10, 11) -> 5*
          f#_1(9, 11) -> 5*
          f#_1(8, 11) -> 5*
         f#_0(10, 10) -> 5*
          f#_0(9, 10) -> 5*
          f#_0(8, 10) -> 5*
          f_2(11, 12) -> 12*
          f_2(10, 11) -> 12*
           f_2(9, 11) -> 12*
           f_2(8, 11) -> 12*
          f_1(11, 13) -> 13 | 11
          f_1(10, 11) -> 11*
          f_1(10, 10) -> 11*
           f_1(9, 10) -> 11*
           f_1(8, 11) -> 13*
           f_1(8, 10) -> 11*
          f_0(10, 10) -> 10*
           f_0(10, 9) -> 10*
           f_0(10, 8) -> 10*
           f_0(9, 10) -> 10*
            f_0(9, 9) -> 10*
            f_0(9, 8) -> 10*
           f_0(8, 10) -> 10*
            f_0(8, 9) -> 10*
            f_0(8, 8) -> 10*
                   10 -> 8*
                    9 -> 8*}
       Strict:
        {f#(f(x, a()), y) -> f#(x, y)}
       EDG:
        {(f#(f(x, a()), y) -> f#(x, y), f#(f(x, a()), y) -> f#(x, y))}
        SCCS:
         Scc:
          {f#(f(x, a()), y) -> f#(x, y)}
         SCC:
          Strict:
           {f#(f(x, a()), y) -> f#(x, y)}
          Weak:
          {f(f(x, a()), y) -> f(y, f(x, y))}
          SPSC:
           Simple Projection:
            pi(f#) = 0
           Strict:
            {}
           Qed