Title: Defining the IEEE-854 Floating-Point Standard in PVS