Definition
M10
:=
Fnum
x10
.
Hypothesis
M10_bound
: 1 <=
M10
<= 10 ^ 16 - 1.
Definition
e10
:=
Fexp
x10
+ 15.
Hypothesis
e10_bound
: -383 <=
e10
<= 384.