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