2.07/1.49 YES 2.07/1.49 2.07/1.49 Proof: 2.07/1.49 This system is confluent. 2.07/1.49 Removed infeasible rules from system R. 2.07/1.49 By \cite{GNG13}, Theorem 9. 2.07/1.49 This system is of type 3 or smaller. 2.07/1.49 This system is deterministic. 2.07/1.49 This system is weakly left-linear. 2.07/1.49 System R transformed to optimized U(R). 2.07/1.49 This system is orthogonal. 2.07/1.49 4.51/2.05 EOF