Definition
M2
:=
Fnum
x2
.
Hypothesis
M2_bound
: 2 ^ 52 <=
M2
<= 2 ^ 53 - 1.
Definition
e2
:=
Fexp
x2
+ 52.
Hypothesis
e2_bound
: -1074 <=
e2
<= 1023.