Problem:
 :(x,x) -> e()
 :(x,e()) -> x
 i(:(x,y)) -> :(y,x)
 :(:(x,y),z) -> :(x,:(z,i(y)))
 :(e(),x) -> i(x)
 i(i(x)) -> x
 i(e()) -> e()
 :(x,:(y,i(x))) -> i(y)
 :(x,:(y,:(i(x),z))) -> :(i(z),y)
 :(i(x),:(y,x)) -> i(y)
 :(i(x),:(y,:(x,z))) -> :(i(z),y)

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