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

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