YES(?,O(n^1)) Problem: f(h(x)) -> f(i(x)) g(i(x)) -> g(h(x)) h(a()) -> b() i(a()) -> b() Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {6,5,4,3} transitions: b1() -> 8* f0(2) -> 3* f0(1) -> 3* h0(2) -> 5* h0(1) -> 5* i0(2) -> 6* i0(1) -> 6* g0(2) -> 4* g0(1) -> 4* a0() -> 1* b0() -> 2* 8 -> 6,5 problem: Qed