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)
  TDG 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)
   graph:
    h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> h#(f(x))
    h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> f#(x)
    h#(g(x)) -> f#(x) -> f#(a()) -> h#(a())
    f#(a()) -> h#(a()) -> h#(g(x)) -> h#(f(x))
    f#(a()) -> h#(a()) -> h#(g(x)) -> f#(x)
   EDG 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)
    graph:
     h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> f#(x)
     h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> h#(f(x))
     h#(g(x)) -> f#(x) -> f#(a()) -> h#(a())
    CDG 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)
     graph:
      h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> h#(f(x))
      h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> f#(x)
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 2/9
      DPs:
       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)
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [h#](x0) = x0 + 0,
        
        [k](x0, x1, x2) = 1x0 + x1 + x2 + 10,
        
        [g](x0) = -1x0 + 1,
        
        [h](x0) = -2x0 + 4,
        
        [f](x0) = -2x0 + 0,
        
        [a] = 7
       orientation:
        h#(g(x)) = -1x + 1 >= -2x + 0 = h#(f(x))
        
        f(a()) = 5 >= 4 = g(h(a()))
        
        h(g(x)) = -3x + 4 >= -5x + 3 = g(h(f(x)))
        
        k(x,h(x),a()) = 1x + 10 >= -2x + 4 = h(x)
        
        k(f(x),y,x) = x + y + 10 >= -2x + 0 = f(x)
       problem:
        DPs:
         
        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)
       Qed