YES Proof: This system is confluent. By \cite{SMI95}, Corollary 4.7 or 5.3. This system is normal. This system is of type 3 or smaller. This system is right-stable. This system is properly oriented. This is an overlay system. This system is left-linear. All 2 critical pairs are trivial or infeasible. true = true <= pos(0) = true: This critical pair is trivial. true = true <= pos(0) = true: This critical pair is trivial. This system is conditional.