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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 28
   0() <-0|[]- +(0(),0()) -1|[]-> 0()
   s(y) <-0|[]- +(0(),s(y)) -3|[]-> s(+(y,0()))
   +(y,z) <-0|[]- +(0(),+(y,z)) -4|[]-> +(+(0(),y),z)
   +(x,z) <-0|1[]- +(x,+(0(),z)) -4|[]-> +(+(x,0()),z)
   y <-0|[]- +(0(),y) -5|[]-> +(y,0())
   0() <-1|[]- +(0(),0()) -0|[]-> 0()
   s(x) <-1|[]- +(s(x),0()) -2|[]-> s(+(0(),x))
   +(x,y) <-1|1[]- +(x,+(y,0())) -4|[]-> +(+(x,y),0())
   x <-1|[]- +(x,0()) -5|[]-> +(0(),x)
   s(+(0(),x133)) <-2|[]- +(s(x133),0()) -1|[]-> s(x133)
   s(+(s(y),x135)) <-2|[]- +(s(x135),s(y)) -3|[]-> s(+(y,s(x135)))
   s(+(+(y,z),x137)) <-2|[]- +(s(x137),+(y,z)) -4|[]-> +(+(s(x137),y),z)
   +(x,s(+(z,x139))) <-2|1[]- +(x,+(s(x139),z)) -4|[]-> +(+(x,s(x139)),z)
   s(+(y,x141)) <-2|[]- +(s(x141),y) -5|[]-> +(y,s(x141))
   s(+(x144,0())) <-3|[]- +(0(),s(x144)) -0|[]-> s(x144)
   s(+(x146,s(x))) <-3|[]- +(s(x),s(x146)) -2|[]-> s(+(s(x146),x))
   +(x,s(+(x148,y))) <-3|1[]- +(x,+(y,s(x148))) -4|[]-> +(+(x,y),s(x148))
   s(+(x150,x)) <-3|[]- +(x,s(x150)) -5|[]-> +(s(x150),x)
   +(+(0(),x152),x153) <-4|[]- +(0(),+(x152,x153)) -0|[]-> +(x152,x153)
   +(+(s(x),x155),x156) <-4|[]- +(s(x),+(x155,x156)) -2|[]-> s(+(+(x155,x156),x))
   +(x,+(+(y,x158),x159)) <-4|1[]- +(x,+(y,+(x158,x159))) -4|[]-> +(+(x,y),+(x158,x159))
   +(+(x,x161),x162) <-4|[]- +(x,+(x161,x162)) -5|[]-> +(+(x161,x162),x)
   +(y,0()) <-5|[]- +(0(),y) -0|[]-> y
   +(0(),x) <-5|[]- +(x,0()) -1|[]-> x
   +(y,s(x)) <-5|[]- +(s(x),y) -2|[]-> s(+(y,x))
   +(s(y),x) <-5|[]- +(x,s(y)) -3|[]-> s(+(y,x))
   +(+(y,z),x) <-5|[]- +(x,+(y,z)) -4|[]-> +(+(x,y),z)
   +(x,+(z,y)) <-5|1[]- +(x,+(y,z)) -4|[]-> +(+(x,y),z)
  Redundant Rules Transformation:
   +(x,0()) -> x
   +(x,s(y)) -> s(+(y,x))
   +(x,+(y,z)) -> +(+(x,y),z)
   +(x,y) -> +(y,x)
   Church Rosser Transformation Processor (ac):
    f4_AC(x,0()) -> x
    f4_AC(x,s(y)) -> s(f4_AC(y,x))
    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