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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 16
  0() <-0|[]- +(0(),0()) -1|[]-> 0()
  s(y) <-0|[]- +(0(),s(y)) -3|[]-> s(+(0(),y))
  y <-0|[]- +(0(),y) -4|[]-> +(y,0())
  0() <-1|[]- +(0(),0()) -0|[]-> 0()
  s(x) <-1|[]- +(s(x),0()) -2|[]-> s(+(x,0()))
  x <-1|[]- +(x,0()) -4|[]-> +(0(),x)
  s(+(x80,0())) <-2|[]- +(s(x80),0()) -1|[]-> s(x80)
  s(+(x82,s(y))) <-2|[]- +(s(x82),s(y)) -3|[]-> s(+(s(x82),y))
  s(+(x84,y)) <-2|[]- +(s(x84),y) -4|[]-> +(y,s(x84))
  s(+(0(),x87)) <-3|[]- +(0(),s(x87)) -0|[]-> s(x87)
  s(+(s(x),x89)) <-3|[]- +(s(x),s(x89)) -2|[]-> s(+(x,s(x89)))
  s(+(x,x91)) <-3|[]- +(x,s(x91)) -4|[]-> +(s(x91),x)
  +(y,0()) <-4|[]- +(0(),y) -0|[]-> y
  +(0(),x) <-4|[]- +(x,0()) -1|[]-> x
  +(y,s(x)) <-4|[]- +(s(x),y) -2|[]-> s(+(x,y))
  +(s(y),x) <-4|[]- +(x,s(y)) -3|[]-> s(+(x,y))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed