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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 0
  Qed