YES # almost development closedness (van Oostrom 1997) Consider the left-linear TRS R: f(a(),a()) -> g(f(a(),a())) a() -> b() f(b(),x) -> g(f(x,x)) f(x,b()) -> g(f(x,x)) R is left-linear and every critical pair is almost development closed