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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   +(s(x),y) -> s(+(x,y))
   +(x,s(y)) -> s(+(x,y))
   +(x,y) -> +(y,x)
  weak:
   
  critical peaks: 6
  s(+(x32,s(y))) <-0|[]- +(s(x32),s(y)) -1|[]-> s(+(s(x32),y))
  s(+(x34,y)) <-0|[]- +(s(x34),y) -2|[]-> +(y,s(x34))
  s(+(s(x),x37)) <-1|[]- +(s(x),s(x37)) -0|[]-> s(+(x,s(x37)))
  s(+(x,x39)) <-1|[]- +(x,s(x39)) -2|[]-> +(s(x39),x)
  +(y,s(x)) <-2|[]- +(s(x),y) -0|[]-> s(+(x,y))
  +(s(y),x) <-2|[]- +(x,s(y)) -1|[]-> s(+(x,y))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed