YES
TRS:
 {h(f(x, y)) -> f(y, f(h(h(x)), a()))}
 DP:
  Strict:
   {h#(f(x, y)) -> h#(x),
    h#(f(x, y)) -> h#(h(x))}
  Weak:
  {h(f(x, y)) -> f(y, f(h(h(x)), a()))}
  EDG:
   {(h#(f(x, y)) -> h#(h(x)), h#(f(x, y)) -> h#(h(x)))
    (h#(f(x, y)) -> h#(h(x)), h#(f(x, y)) -> h#(x))
    (h#(f(x, y)) -> h#(x), h#(f(x, y)) -> h#(x))
    (h#(f(x, y)) -> h#(x), h#(f(x, y)) -> h#(h(x)))}
   SCCS:
    Scc:
     {h#(f(x, y)) -> h#(x),
      h#(f(x, y)) -> h#(h(x))}
    SCC:
     Strict:
      {h#(f(x, y)) -> h#(x),
       h#(f(x, y)) -> h#(h(x))}
     Weak:
     {h(f(x, y)) -> f(y, f(h(h(x)), a()))}
     BOUND:
      Bound: match(-raise)-bounded by 1
      Automaton:
       {     b_0() -> 2*
             a_1() -> 9*
             a_0() -> 5*
           h#_1(2) -> 8*
           h#_0(3) -> 8*
           h#_0(2) -> 8 | 7
            h_1(2) -> 2*
            h_0(3) -> 4*
            h_0(2) -> 3*
        f_1(6, 10) -> 4*
         f_1(2, 9) -> 10*
         f_0(6, 6) -> 4*
         f_0(4, 5) -> 6*
         f_0(2, 6) -> 1*
                 8 -> 7*
                 1 -> 3*}
      Strict:
       {}
      Qed