YES

Problem:
 f(a()) -> g(h(a()))
 h(g(x)) -> g(h(f(x)))
 k(x,h(x),a()) -> h(x)
 k(f(x),y,x) -> f(x)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {14,13,6,8,4,1}
   transitions:
    f50() -> 5*
    g0(12) -> 7*
    g0(7) -> 13*,8,4
    g0(3) -> 14*,6,1
    h0(5) -> 8*
    h0(2) -> 3*
    h0(14) -> 7*
    h0(11) -> 12*
    h0(6) -> 7*
    a0() -> 2*
    f0(5) -> 6*
    f0(3) -> 11*
    g1(12) -> 7*
    h1(11) -> 12*
    f1(3) -> 11*
    1 -> 6*
    4 -> 8*
  problem:
   
  Qed