HOL.Semiring_Normalization