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