Problem: h(f(f(x))) -> h(f(g(f(x)))) f(g(f(x))) -> f(f(x)) Proof: Bounds Processor: bound: 0 enrichment: match automaton: final states: {3,2} transitions: h0(1) -> 2* f0(1) -> 3* g0(1) -> 1* problem: Qed