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

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {6,5,4,3,2}
   transitions:
    active0(1) -> 2*
    f0(1) -> 4*
    mark0(1) -> 3*
    g0(1) -> 5*
    h0(1) -> 6*
    f100() -> 1*
  problem:
   
  Qed