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

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