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

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