YES

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

Proof:
 Church Rosser Transformation Processor (okui):
  
  simultaneous critical peaks: 
   *(+(y,x),z)
    <-[0]- *(+(x,y),z) -[]->
   +(*(x,z),*(y,z))
   
   +(*(x,x69),*(y,x69))
    <-[]- *(+(x,y),x69) -[0]->
   *(+(y,x),x69)
   joinable
  Qed