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

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