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

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