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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 36
   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())
   dbl(y) <-0|0[]- dbl(+(0(),y)) -7|[]-> +(dbl(0()),dbl(y))
   0() <-1|[]- +(0(),0()) -0|[]-> 0()
   s(x) <-1|[]- +(s(x),0()) -2|[]-> s(+(x,0()))
   +(x,y) <-1|1[]- +(x,+(y,0())) -4|[]-> +(+(x,y),0())
   x <-1|[]- +(x,0()) -5|[]-> +(0(),x)
   dbl(x) <-1|0[]- dbl(+(x,0())) -7|[]-> +(dbl(x),dbl(0()))
   s(+(x210,0())) <-2|[]- +(s(x210),0()) -1|[]-> s(x210)
   s(+(x212,s(y))) <-2|[]- +(s(x212),s(y)) -3|[]-> +(s(y),s(x212))
   s(+(x214,+(y,z))) <-2|[]- +(s(x214),+(y,z)) -4|[]-> +(+(s(x214),y),z)
   +(x,s(+(x216,z))) <-2|1[]- +(x,+(s(x216),z)) -4|[]-> +(+(x,s(x216)),z)
   s(+(x218,y)) <-2|[]- +(s(x218),y) -5|[]-> +(y,s(x218))
   dbl(s(+(x220,y))) <-2|0[]- dbl(+(s(x220),y)) -7|[]-> +(dbl(s(x220)),dbl(y))
   +(s(x223),0()) <-3|[]- +(0(),s(x223)) -0|[]-> s(x223)
   +(s(x225),s(x)) <-3|[]- +(s(x),s(x225)) -2|[]-> s(+(x,s(x225)))
   +(x,+(s(x227),y)) <-3|1[]- +(x,+(y,s(x227))) -4|[]-> +(+(x,y),s(x227))
   +(s(x229),x) <-3|[]- +(x,s(x229)) -5|[]-> +(s(x229),x)
   dbl(+(s(x231),x)) <-3|0[]- dbl(+(x,s(x231))) -7|[]-> +(dbl(x),dbl(s(x231)))
   +(+(0(),x233),x234) <-4|[]- +(0(),+(x233,x234)) -0|[]-> +(x233,x234)
   +(+(s(x),x236),x237) <-4|[]- +(s(x),+(x236,x237)) -2|[]-> s(+(x,+(x236,x237)))
   +(x,+(+(y,x239),x240)) <-4|1[]- +(x,+(y,+(x239,x240))) -4|[]-> +(+(x,y),+(x239,x240))
   +(+(x,x242),x243) <-4|[]- +(x,+(x242,x243)) -5|[]-> +(+(x242,x243),x)
   dbl(+(+(x,x245),x246)) <-4|0[]- dbl(+(x,+(x245,x246))) -7|[]-> +(dbl(x),dbl(+(x245,x246)))
   +(y,0()) <-5|[]- +(0(),y) -0|[]-> y
   +(0(),x) <-5|[]- +(x,0()) -1|[]-> x
   +(y,s(x)) <-5|[]- +(s(x),y) -2|[]-> s(+(x,y))
   +(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)
   dbl(+(y,x)) <-5|0[]- dbl(+(x,y)) -7|[]-> +(dbl(x),dbl(y))
   +(+(x,y),+(x,y)) <-6|[]- dbl(+(x,y)) -7|[]-> +(dbl(x),dbl(y))
   +(dbl(x262),dbl(x263)) <-7|[]- dbl(+(x262,x263)) -6|[]-> +(+(x262,x263),+(x262,x263))
  Redundant Rules Transformation:
   +(x,0()) -> x
   +(s(x),y) -> s(+(x,y))
   +(x,+(y,z)) -> +(+(x,y),z)
   +(x,y) -> +(y,x)
   dbl(x) -> +(x,x)
   Church Rosser Transformation Processor (ac):
    f5_AC(x,0()) -> x
    f5_AC(s(x),y) -> s(f5_AC(x,y))
    dbl(x) -> f5_AC(x,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