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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
  weak:
   
  critical peaks: 8
  0() <-0|[]- +(0(),0()) -2|[]-> 0()
  s(y) <-0|[]- +(0(),s(y)) -3|[]-> s(+(0(),y))
  s(+(x52,0())) <-1|[]- +(s(x52),0()) -2|[]-> s(x52)
  s(+(x54,s(y))) <-1|[]- +(s(x54),s(y)) -3|[]-> s(+(s(x54),y))
  0() <-2|[]- +(0(),0()) -0|[]-> 0()
  s(x) <-2|[]- +(s(x),0()) -1|[]-> s(+(x,0()))
  s(+(0(),x59)) <-3|[]- +(0(),s(x59)) -0|[]-> s(x59)
  s(+(s(x),x61)) <-3|[]- +(s(x),s(x61)) -1|[]-> s(+(x,s(x61)))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed