YES(?,O(n^1))

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: {9,8,7,3,2}
   transitions:
    :0(8,1) -> 2*
    :0(8,7) -> 2*
    :0(1,8) -> 2*
    :0(7,1) -> 2*
    :0(7,7) -> 2*
    :0(8,8) -> 2*
    :0(1,1) -> 2*
    :0(1,7) -> 2*
    :0(7,8) -> 2*
    e0() -> 7*,2,1
    i0(7) -> 3*
    i0(1) -> 3*
    i0(8) -> 3*
    e1() -> 7,9,8*,1,3,2
    i1(7) -> 2,3,9*
    i1(1) -> 9*,3,2
    i1(8) -> 2,3,9*
    e2() -> 9,7,2,3,1,8*
    1 -> 2*
    7 -> 2*
    8 -> 2*
  problem:
   
  Qed