YES

# almost development closedness (van Oostrom 1997)

Consider the left-linear TRS R:

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

R is left-linear and every critical pair is almost development closed