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

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