YES(?,O(n^1)) Problem: f(a()) -> f(b()) g(b()) -> g(a()) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {4,3} transitions: g1(9) -> 10* a1() -> 9* f1(7) -> 8* b1() -> 7* f0(2) -> 3* f0(1) -> 3* a0() -> 1* b0() -> 2* g0(2) -> 4* g0(1) -> 4* 8 -> 3* 10 -> 4* problem: Qed