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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 4
  *(+(y,x),z) <-0|0[]- *(+(x,y),z) -1|[]-> +(*(x,z),*(y,z))
  *(+(x,y),z) <-0|0[]- *(+(y,x),z) -2|[]-> +(*(x,z),*(y,z))
  +(*(y,z),*(x,z)) <-1|[]- *(+(y,x),z) -2|[]-> +(*(x,z),*(y,z))
  +(*(y,z),*(x,z)) <-2|[]- *(+(x,y),z) -1|[]-> +(*(x,z),*(y,z))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed