Problem:
 \(x,x) -> e()
 /(x,x) -> e()
 .(e(),x) -> x
 .(x,e()) -> x
 \(e(),x) -> x
 /(x,e()) -> x
 .(x,\(x,y)) -> y
 .(/(y,x),x) -> y
 \(x,.(x,y)) -> y
 /(.(y,x),x) -> y
 /(x,\(y,x)) -> y
 \(/(x,y),x) -> y

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {5,4,3,2}
   transitions:
    e1() -> 5*,4,1,3,2
    \0(5,1) -> 2*
    \0(5,5) -> 2*
    \0(1,1) -> 2*
    \0(1,5) -> 2*
    /0(5,1) -> 3*
    /0(5,5) -> 3*
    /0(1,1) -> 3*
    /0(1,5) -> 3*
    .0(5,1) -> 4*
    .0(5,5) -> 4*
    .0(1,1) -> 4*
    .0(1,5) -> 4*
    1 -> 3,2,4
    5 -> 3,2,4
  problem:
   
  Qed