Problem: f(f(X)) -> c() c() -> d() h(X) -> c() Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {4,3,2} transitions: c1() -> 7* d1() -> 6* d2() -> 10* f0(1) -> 2* c0() -> 3* d0() -> 1* h0(1) -> 4* 6 -> 3* 7 -> 4* 10 -> 7,4 problem: Qed