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

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