YES

Problem:
 a__f(X) -> g(h(f(X)))
 mark(f(X)) -> a__f(mark(X))
 mark(g(X)) -> g(X)
 mark(h(X)) -> h(mark(X))
 a__f(X) -> f(X)

Proof:
 DP Processor:
  DPs:
   mark#(f(X)) -> mark#(X)
   mark#(f(X)) -> a__f#(mark(X))
   mark#(h(X)) -> mark#(X)
  TRS:
   a__f(X) -> g(h(f(X)))
   mark(f(X)) -> a__f(mark(X))
   mark(g(X)) -> g(X)
   mark(h(X)) -> h(mark(X))
   a__f(X) -> f(X)
  Arctic Interpretation Processor:
   dimension: 1
   usable rules:
    
   interpretation:
    [mark#](x0) = 8x0 + -15,
    
    [a__f#](x0) = 0,
    
    [mark](x0) = x0 + -16,
    
    [g](x0) = -12x0 + 0,
    
    [h](x0) = 4x0 + 8,
    
    [f](x0) = 3x0 + 8,
    
    [a__f](x0) = 6x0 + -16
   orientation:
    mark#(f(X)) = 11X + 16 >= 8X + -15 = mark#(X)
    
    mark#(f(X)) = 11X + 16 >= 0 = a__f#(mark(X))
    
    mark#(h(X)) = 12X + 16 >= 8X + -15 = mark#(X)
    
    a__f(X) = 6X + -16 >= -5X + 0 = g(h(f(X)))
    
    mark(f(X)) = 3X + 8 >= 6X + -10 = a__f(mark(X))
    
    mark(g(X)) = -12X + 0 >= -12X + 0 = g(X)
    
    mark(h(X)) = 4X + 8 >= 4X + 8 = h(mark(X))
    
    a__f(X) = 6X + -16 >= 3X + 8 = f(X)
   problem:
    DPs:
     
    TRS:
     a__f(X) -> g(h(f(X)))
     mark(f(X)) -> a__f(mark(X))
     mark(g(X)) -> g(X)
     mark(h(X)) -> h(mark(X))
     a__f(X) -> f(X)
   Qed