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

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