Title: High-Level Formalization of Floating-Point Number in PVS