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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 36
   0() <-0|[]- +(0(),0()) -2|[]-> 0()
   s(x) <-0|[]- +(s(x),0()) -3|[]-> s(+(x,0()))
   +(x,y) <-0|[]- +(+(x,y),0()) -5|[]-> +(x,+(y,0()))
   +(x,z) <-0|0[]- +(+(x,0()),z) -5|[]-> +(x,+(0(),z))
   x <-0|[]- +(x,0()) -6|[]-> +(0(),x)
   s(+(0(),x219)) <-1|[]- +(0(),s(x219)) -2|[]-> s(x219)
   s(+(s(x),x221)) <-1|[]- +(s(x),s(x221)) -3|[]-> s(+(x,s(x221)))
   s(+(+(x,y),x223)) <-1|[]- +(+(x,y),s(x223)) -5|[]-> +(x,+(y,s(x223)))
   +(s(+(x,x225)),z) <-1|0[]- +(+(x,s(x225)),z) -5|[]-> +(x,+(s(x225),z))
   s(+(x,x227)) <-1|[]- +(x,s(x227)) -6|[]-> +(s(x227),x)
   0() <-2|[]- +(0(),0()) -0|[]-> 0()
   s(y) <-2|[]- +(0(),s(y)) -1|[]-> s(+(0(),y))
   +(y,z) <-2|0[]- +(+(0(),y),z) -5|[]-> +(0(),+(y,z))
   y <-2|[]- +(0(),y) -6|[]-> +(y,0())
   s(+(x232,0())) <-3|[]- +(s(x232),0()) -0|[]-> s(x232)
   s(+(x234,s(y))) <-3|[]- +(s(x234),s(y)) -1|[]-> s(+(s(x234),y))
   +(s(+(x236,y)),z) <-3|0[]- +(+(s(x236),y),z) -5|[]-> +(s(x236),+(y,z))
   s(+(x238,y)) <-3|[]- +(s(x238),y) -6|[]-> +(y,s(x238))
   +(x240,+(x241,0())) <-5|[]- +(+(x240,x241),0()) -0|[]-> +(x240,x241)
   +(x243,+(x244,s(y))) <-5|[]- +(+(x243,x244),s(y)) -1|[]-> s(+(+(x243,x244),y))
   +(+(x246,+(x247,y)),z) <-5|0[]- +(+(+(x246,x247),y),z) -5|[]-> +(+(x246,x247),+(y,z))
   +(x249,+(x250,y)) <-5|[]- +(+(x249,x250),y) -6|[]-> +(y,+(x249,x250))
   +(0(),x) <-6|[]- +(x,0()) -0|[]-> x
   +(s(y),x) <-6|[]- +(x,s(y)) -1|[]-> s(+(x,y))
   +(y,0()) <-6|[]- +(0(),y) -2|[]-> y
   +(y,s(x)) <-6|[]- +(s(x),y) -3|[]-> s(+(x,y))
   +(z,+(x,y)) <-6|[]- +(+(x,y),z) -5|[]-> +(x,+(y,z))
   +(+(y,x),z) <-6|0[]- +(+(x,y),z) -5|[]-> +(x,+(y,z))
   +(x,s(s(y))) <-7|1[]- +(x,s(y)) -1|[]-> s(+(x,y))
   +(s(s(x)),y) <-7|0[]- +(s(x),y) -3|[]-> s(+(x,y))
   s(s(s(x))) <-7|[]- s(s(x)) -8|[]-> s(x)
   s(s(s(x))) <-7|0[]- s(s(x)) -8|[]-> s(x)
   +(x,s(x268)) <-8|1[]- +(x,s(s(x268))) -1|[]-> s(+(x,s(x268)))
   +(s(x269),y) <-8|0[]- +(s(s(x269)),y) -3|[]-> s(+(s(x269),y))
   s(x270) <-8|[]- s(s(x270)) -7|[]-> s(s(s(x270)))
   s(s(x271)) <-8|0[]- s(s(s(x271))) -8|[]-> s(s(x271))
  Redundant Rules Transformation:
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   dbl(x) -> +(x,x)
   +(+(x,y),z) -> +(x,+(y,z))
   +(x,y) -> +(y,x)
   s(s(x)) -> s(x)
   Church Rosser Transformation Processor (ac):
    f5_AC(0(),y) -> y
    f5_AC(s(x),y) -> s(f5_AC(x,y))
    dbl(x) -> f5_AC(x,x)
    s(s(x)) -> s(x)
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      dbl > f5_AC > s ~ 0
      weight function:
       [dbl](x0) = 2x0 + 2,
       
       [f5_AC](x0, x1) = x0 + x1 + 2,
       
       [0] = 1,
       
       [s](x0) = x0 + 2
      problem:
       
      Qed