YES(?,O(n^1)) Problem: w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {3,2} transitions: r1(11) -> 12* r1(8) -> 9* b1(10) -> 11* w1(7) -> 8* w0(1) -> 2* r0(1) -> 1* b0(1) -> 3* 1 -> 10,7 9 -> 8,2 12 -> 11,3 problem: Qed