In order for a significand, which has the form
The definition may be restated as follows.
The next three lemmas are consequences of the observation that -exactness of is a property of .
PROOF: By Lemma 4.1.13, .
PROOF: By Lemma 4.1.14, .
It is clear that is is representable in a given field of bits, then it is also representable in any wider field.
PROOF: Since and ,
Any power of 2 has a 1-bit significand.
PROOF: By Lemma 4.1.4,
A bit vector is exact with respect to its width.
PROOF: Since 0 is -exact for all , we may assume , and therefore . Now since , Lemma 4.1.3 implies , and hence .
We have the following formula for the exactness of a product.
PROOF: If and are integers, then by Lemma 4.1.15, so is
In particular, if is -exact, then is -exact. The converse also holds.
PROOF: We shall require an elementary fact of arithmetic:
Now to show that is -exact, i.e., , it will suffice to show that
PROOF: Let and be the smallest integers such that and are integers. Thus, and are odd. By Lemma 4.2.4, , , or , respectively, is -exact iff , , or is -exact. Consequently,, we may replace and with and . That is, we may assume without loss of generality that and are odd integers.
By Lemma 4.2.1, an odd integer is -exact iff , or equivalently, acording to Lemma 4.1.3, . Thus, since is -exact, , which implies and , and hence and are -exact.
Exactness of a bit vector may be formulated in various ways.
|(a) is -exact|
PROOF: The equivalence between (a) and (b) follows from Lemma 4.2.1, since
The next lemma gives a formula for exactness of a difference.
PROOF: Since is -exact and ,
Lemma 4.2.13 is often applied with , in the following weaker form.
If is positive and -exact, then the least -exact number exceeding is computed as follows.
PROOF: Let and . Since is -exact, , and by Lemma 4.1.3, . Thus,
PROOF: Let and . Since is -exact, . Similar, since is -exact, . But by Corollary 4.1.5, and hence
PROOF: Since , Lemma 4.1.5 implies . Therefore, we have , which, according to Lemma 4.1.3, implies . On the other hand, since is -exact by Lemma 4.2.6, Lemma 4.2.16 implies .
PROOF: Since the case is trivial, we shall assume that and, without loss of generality, that . But then by Lemma 4.2.16,
Similarly, the following definition computes the greatest -exact number that is less than a given -exact number.
PROOF: Let and .
Suppose first that . Then , and since
Now suppose . Then by Lemma 4.2.15,
PROOF: Let , and . We shall prove first that .
As noted in the proof of Lemma 4.2.15,
Next, we prove that . Note that . If , then , and since ,
PROOF: Suppose . Then since and are both -exact, Lemma 4.2.15 implies , a contradiction.
David Russinoff 2017-08-01