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