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)
 dbl(+(x,y)) -> +(dbl(x),dbl(y))

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)
   dbl(x) <-0|0[]- dbl(+(x,0())) -7|[]-> +(dbl(x),dbl(0()))
   s(+(0(),x206)) <-1|[]- +(0(),s(x206)) -2|[]-> s(x206)
   s(+(s(x),x208)) <-1|[]- +(s(x),s(x208)) -3|[]-> s(+(x,s(x208)))
   s(+(+(x,y),x210)) <-1|[]- +(+(x,y),s(x210)) -5|[]-> +(x,+(y,s(x210)))
   +(s(+(x,x212)),z) <-1|0[]- +(+(x,s(x212)),z) -5|[]-> +(x,+(s(x212),z))
   s(+(x,x214)) <-1|[]- +(x,s(x214)) -6|[]-> +(s(x214),x)
   dbl(s(+(x,x216))) <-1|0[]- dbl(+(x,s(x216))) -7|[]-> +(dbl(x),dbl(s(x216)))
   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())
   dbl(y) <-2|0[]- dbl(+(0(),y)) -7|[]-> +(dbl(0()),dbl(y))
   s(+(x222,0())) <-3|[]- +(s(x222),0()) -0|[]-> s(x222)
   s(+(x224,s(y))) <-3|[]- +(s(x224),s(y)) -1|[]-> s(+(s(x224),y))
   +(s(+(x226,y)),z) <-3|0[]- +(+(s(x226),y),z) -5|[]-> +(s(x226),+(y,z))
   s(+(x228,y)) <-3|[]- +(s(x228),y) -6|[]-> +(y,s(x228))
   dbl(s(+(x230,y))) <-3|0[]- dbl(+(s(x230),y)) -7|[]-> +(dbl(s(x230)),dbl(y))
   +(+(x,y),+(x,y)) <-4|[]- dbl(+(x,y)) -7|[]-> +(dbl(x),dbl(y))
   +(x233,+(x234,0())) <-5|[]- +(+(x233,x234),0()) -0|[]-> +(x233,x234)
   +(x236,+(x237,s(y))) <-5|[]- +(+(x236,x237),s(y)) -1|[]-> s(+(+(x236,x237),y))
   +(+(x239,+(x240,y)),z) <-5|0[]- +(+(+(x239,x240),y),z) -5|[]-> +(+(x239,x240),+(y,z))
   +(x242,+(x243,y)) <-5|[]- +(+(x242,x243),y) -6|[]-> +(y,+(x242,x243))
   dbl(+(x245,+(x246,y))) <-5|0[]- dbl(+(+(x245,x246),y)) -7|[]-> +(dbl(+(x245,x246)),dbl(y))
   +(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))
   dbl(+(y,x)) <-6|0[]- dbl(+(x,y)) -7|[]-> +(dbl(x),dbl(y))
   +(dbl(x262),dbl(x263)) <-7|[]- dbl(+(x262,x263)) -4|[]-> +(+(x262,x263),+(x262,x263))
  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)
   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)
    AC critical peaks: joinable
    AC-RPO Processor:
     precedence:
      dbl > 0 > f5_AC > s
     status:
      
     problem:
      
     Qed