Problem:
 join(x,x) -> x
 join(x,y) -> join(y,x)
 join(join(x,y),z) -> join(x,join(y,z))

Proof:
 Church Rosser Transformation Processor (ac):
  f2_AC(x,x) -> x
  AC critical peaks: joinable
  AC-KBO Processor:
   precedence:
    f2_AC
    weight function:
     w0 = 2
     w(f2_AC) = 0
    problem:
     
    Qed