YES(?,O(n^1)) Problem: h(f(x),y) -> f(g(x,y)) g(x,y) -> h(x,y) Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {3,2} transitions: h1(1,1) -> 3* f1(4) -> 4,3,2 g1(1,1) -> 4* h2(1,1) -> 4* h0(1,1) -> 2* f0(1) -> 1* g0(1,1) -> 3* problem: Qed