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

Proof:
 Church Rosser Transformation Processor (ac):
  f4_AC(0(),y) -> y
  f4_AC(x,0()) -> x
  f4_AC(s(x),y) -> s(f4_AC(y,x))
  f4_AC(x,s(y)) -> s(f4_AC(x,y))
  AC critical peaks: joinable
  AC-KBO Processor:
   precedence:
    f4_AC > s > 0
    weight function:
     w0 = 4
     w(0) = 4
     w(s) = 2
     w(f4_AC) = 0
    problem:
     
    Qed