Problem: active(f(f(X))) -> mark(c(f(g(f(X))))) active(c(X)) -> mark(d(X)) active(h(X)) -> mark(c(d(X))) mark(f(X)) -> active(f(mark(X))) mark(c(X)) -> active(c(X)) mark(g(X)) -> active(g(X)) mark(d(X)) -> active(d(X)) mark(h(X)) -> active(h(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) d(mark(X)) -> d(X) d(active(X)) -> d(X) h(mark(X)) -> h(X) h(active(X)) -> h(X) Proof: Bounds Processor: bound: 0 enrichment: match automaton: final states: {8,7,6,5,4,3,2} transitions: active0(1) -> 2* f0(1) -> 4* mark0(1) -> 3* c0(1) -> 5* g0(1) -> 6* d0(1) -> 7* h0(1) -> 8* f140() -> 1* problem: Qed