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)
  TDG 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)
   graph:
    mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> mark#(X)
    mark#(h(X)) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X))
    mark#(h(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
    mark#(f(X)) -> mark#(X) -> mark#(h(X)) -> mark#(X)
    mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X))
    mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 6/9
    DPs:
     mark#(h(X)) -> mark#(X)
     mark#(f(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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [mark#](x0) = x0,
      
      [mark](x0) = x0,
      
      [g](x0) = x0,
      
      [h](x0) = x0,
      
      [f](x0) = x0 + 1,
      
      [a__f](x0) = x0 + 1
     orientation:
      mark#(h(X)) = X >= X = mark#(X)
      
      mark#(f(X)) = X + 1 >= X = mark#(X)
      
      a__f(X) = X + 1 >= X + 1 = g(h(f(X)))
      
      mark(f(X)) = X + 1 >= X + 1 = a__f(mark(X))
      
      mark(g(X)) = X >= X = g(X)
      
      mark(h(X)) = X >= X = h(mark(X))
      
      a__f(X) = X + 1 >= X + 1 = f(X)
     problem:
      DPs:
       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)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [mark#](x0) = x0 + 1,
       
       [mark](x0) = x0,
       
       [g](x0) = 0,
       
       [h](x0) = x0 + 1,
       
       [f](x0) = 1,
       
       [a__f](x0) = 1
      orientation:
       mark#(h(X)) = X + 2 >= X + 1 = mark#(X)
       
       a__f(X) = 1 >= 0 = g(h(f(X)))
       
       mark(f(X)) = 1 >= 1 = a__f(mark(X))
       
       mark(g(X)) = 0 >= 0 = g(X)
       
       mark(h(X)) = X + 1 >= X + 1 = h(mark(X))
       
       a__f(X) = 1 >= 1 = 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