YES

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

Proof:
 Church Rosser Transformation Processor:
  strict:
   -(0(),0()) -> 0()
   -(s(x),0()) -> s(x)
   -(x,s(y)) -> -(d(x),y)
   d(s(x)) -> x
   -(s(x),s(y)) -> -(x,y)
   -(d(x),y) -> -(x,s(y))
  weak:
   
  critical peaks: 5
   -(d(s(x)),y) <-2|[]- -(s(x),s(y)) -4|[]-> -(x,y)
   -(d(d(x)),x125) <-2|[]- -(d(x),s(x125)) -5|[]-> -(x,s(s(x125)))
   -(x126,y) <-3|0[]- -(d(s(x126)),y) -5|[]-> -(s(x126),s(y))
   -(x127,y) <-4|[]- -(s(x127),s(y)) -2|[]-> -(d(s(x127)),y)
   -(x129,s(s(y))) <-5|[]- -(d(x129),s(y)) -2|[]-> -(d(d(x129)),y)
  Closedness Processor (*strongly -- <=7 steps*):
   strict:
    
   weak:
    
   Qed