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