Problem:
 a(0(),b(0(),x)) -> b(0(),a(0(),x))
 a(0(),x) -> b(0(),b(0(),x))
 a(0(),a(1(),a(x,y))) -> a(1(),a(0(),a(x,y)))
 b(0(),a(1(),a(x,y))) -> b(1(),a(0(),a(x,y)))
 a(0(),a(x,y)) -> a(1(),a(1(),a(x,y)))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    b1(7,1) -> 8*
    b1(7,2) -> 8*
    b1(7,8) -> 3*
    01() -> 7*
    a0(1,2) -> 3*
    a0(2,1) -> 3*
    a0(1,1) -> 3*
    a0(2,2) -> 3*
    00() -> 1*
    b0(1,2) -> 4*
    b0(2,1) -> 4*
    b0(1,1) -> 4*
    b0(2,2) -> 4*
    10() -> 2*
  problem:
   
  Qed