YES Proof: This system is confluent. By \cite{GNG13}, Theorem 9. This system is deterministic. This system is weakly left-linear. System R transformed to optimized U(R). This system is orthogonal.