YES # strong closedness (Huet 1980) Consider the left-linear TRS R: W(W(x)) -> W(x) B(I(x)) -> W(x) W(B(x)) -> B(x) F(H(x),y) -> F(H(x),G(y)) F(x,I(y)) -> F(G(x),I(y)) G(x) -> x R is linear and every critical pair is strongly closed