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

Proof:
 Church Rosser Transformation Processor (ac):
  *(f3_AC(x,y),z) -> f3_AC(*(x,z),*(y,z))
  *(x,f3_AC(y,z)) -> f3_AC(*(x,y),*(x,z))
  AC critical peaks: joinable
  AC-RPO Processor:
   precedence:
    * > f3_AC
   status:
    *:mul  
   problem:
    
   Qed