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:
 DP Processor:
  DPs:
   f#(a()) -> h#(a())
   h#(g(x)) -> f#(x)
   h#(g(x)) -> h#(f(x))
  TRS:
   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)
  Usable Rule Processor:
   DPs:
    f#(a()) -> h#(a())
    h#(g(x)) -> f#(x)
    h#(g(x)) -> h#(f(x))
   TRS:
    f(a()) -> g(h(a()))
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     f(a()) -> g(h(a()))
    interpretation:
     [h#](x0) = x0,
     
     [f#](x0) = 1x0,
     
     [g](x0) = 2x0,
     
     [h](x0) = -2x0 + 0,
     
     [f](x0) = 1x0,
     
     [a] = 2
    orientation:
     f#(a()) = 3 >= 2 = h#(a())
     
     h#(g(x)) = 2x >= 1x = f#(x)
     
     h#(g(x)) = 2x >= 1x = h#(f(x))
     
     f(a()) = 3 >= 2 = g(h(a()))
    problem:
     DPs:
      
     TRS:
      f(a()) -> g(h(a()))
    Qed