Problem:
 +(x,y) -> +(y,x)

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  
  critical peaks: joinable
  Qed