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)
  String Reversal Processor:
   a__f(X) -> f(h(g(X)))
   f(mark(X)) -> mark(a__f(X))
   h(mark(X)) -> mark(h(X))
   a__f(X) -> f(X)
   Bounds Processor:
    bound: 1
    enrichment: match
    automaton:
     final states: {9,7,5,1}
     transitions:
      f50() -> 2*
      f0(2) -> 9*
      f0(4) -> 1*
      h0(2) -> 8*
      h0(3) -> 4*
      g0(2) -> 3*
      mark0(6) -> 5*
      mark0(8) -> 7*
      a__f0(2) -> 6*
      f1(16) -> 17*
      f1(18) -> 19*
      h1(15) -> 16*
      g1(14) -> 15*
      2 -> 18,14
      5 -> 19,9,6
      7 -> 8*
      17 -> 6*
      19 -> 6*
    problem:
     
    Qed