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:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {3,8,7,5,1}
   transitions:
    f50() -> 2*
    g0(2) -> 7*
    g0(4) -> 1*
    h0(6) -> 8*
    h0(3) -> 4*
    f0(2) -> 3*
    a__f0(6) -> 5*
    mark0(2) -> 6*
    f1(13) -> 14*
    g1(15) -> 16*
    h1(14) -> 15*
    5 -> 6,13
    6 -> 13*
    7 -> 6,13
    8 -> 6,13
    14 -> 5*
    16 -> 5*
  problem:
   
  Qed