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:
 Arctic Interpretation Processor:
  dimension: 2
  interpretation:
                [0 2]  
   [mark](x0) = [0 1]x0,
   
             [0  -&]  
   [g](x0) = [0  -&]x0,
   
               
   [h](x0) = x0,
   
             [0  -&]  
   [f](x0) = [0  1 ]x0,
   
                [0 0]  
   [a__f](x0) = [0 1]x0
  orientation:
             [0 0]     [0  -&]              
   a__f(X) = [0 1]X >= [0  -&]X = g(h(f(X)))
   
                [2 3]     [0 2]                 
   mark(f(X)) = [1 2]X >= [1 2]X = a__f(mark(X))
   
                [2  -&]     [0  -&]        
   mark(g(X)) = [1  -&]X >= [0  -&]X = g(X)
   
                [0 2]     [0 2]              
   mark(h(X)) = [0 1]X >= [0 1]X = h(mark(X))
   
             [0 0]     [0  -&]        
   a__f(X) = [0 1]X >= [0  1 ]X = f(X)
  problem:
   a__f(X) -> g(h(f(X)))
   mark(f(X)) -> a__f(mark(X))
   mark(h(X)) -> h(mark(X))
   a__f(X) -> f(X)
  Arctic Interpretation Processor:
   dimension: 2
   interpretation:
                 [0 2]  
    [mark](x0) = [1 2]x0,
    
              [0  -&]  
    [g](x0) = [-& -&]x0,
    
              [0  -&]  
    [h](x0) = [0  1 ]x0,
    
              [0  -&]  
    [f](x0) = [2  3 ]x0,
    
                 [1 3]  
    [a__f](x0) = [2 3]x0
   orientation:
              [1 3]     [0  -&]              
    a__f(X) = [2 3]X >= [-& -&]X = g(h(f(X)))
    
                 [4 5]     [4 5]                 
    mark(f(X)) = [4 5]X >= [4 5]X = a__f(mark(X))
    
                 [2 3]     [0 2]              
    mark(h(X)) = [2 3]X >= [2 3]X = h(mark(X))
    
              [1 3]     [0  -&]        
    a__f(X) = [2 3]X >= [2  3 ]X = f(X)
   problem:
    mark(f(X)) -> a__f(mark(X))
    mark(h(X)) -> h(mark(X))
    a__f(X) -> f(X)
   KBO Processor:
    weight function:
     w0 = 1
     w(mark) = w(h) = w(f) = w(a__f) = 1
    precedence:
     mark > a__f > h ~ f
    problem:
     
    Qed