Since bitn is defined as a special case of bits, we discuss the latter function first.
PROOF: By Lemmas 1.1.1 and 1.2.2, . By Lemma 1.2.3,
Example: Let . Then
is a 3-bit vector and
is a 4-bit vector.
PROOF: By Lemma 1.2.21, .
If the lower limit of a bit slice is 0, it reduces to a call to :
Calls to bits may often be eliminated by means of the following.
PROOF: Since , by Lemmas 2.2.4 and 1.2.6,
Lemma 2.2.5 may be generalized to cover negative bit vectors:
PROOF: For , by Lemmas 2.2.4, 1.2.15, and 1.2.6,
If , then is the bit vector of width consisting of all 1's:
PROOF: By Lemmas 2.2.4 and 1.2.15, . Thus, by Definition 2.0.1, Lemma 1.1.4, and Definition 1.1.1,
The following results are derived from corresponding properties of mod.
PROOF: By Definition 2.0.1 and Lemmas 1.2.18 and 1.2.20,
By expanding , we may express a bit slice in terms of the floor alone:
PROOF: Applying Definitions 2.0.1 and 1.2.1 and Lemma 1.1.4, we have
PROOF: This follows from Definition 1.2.1 and Lemmas 2.2.10 and 1.1.5:
In most cases of interest, the index arguments of satisfy . However, the following two lemmas are worth noting.
Definition 1.2.1 and Lemma 1.1.1, we have
PROOF: By Lemma 1.2.3,
Here is another case in which a bit slice may be reduced to 0:
PROOF: By Lemmas 1.2.2 and 1.2.5,
According to our next lemma, a slice of a right-shifted bit vector, , may always be represented as a slice of .
PROOF: Let and , so that and . Then
PROOF: Applying Lemma 2.2.16, Definition 2.0.1, and Lemma 2.2.4 in succession, we have
PROOF: If , then by Definition 2.0.1 and Lemma 1.2.22,
The next lemma provides an alternate expression for a left-shifted bit slice with lower limit 0:
PROOF: By Lemmas 1.2.22 and 2.2.4,
We note two cases in which a bit slice of can be simplified.
PROOF: By Lemma 2.2.13, we may assume that . Since ,
PROOF: Since , where , Lemma 1.2.15 implies The lemma now follows from Lemma 2.2.2.
Here is an important lemma that decomposes a slice into two subslices.
PROOF: The proof consists of three applications of Lemma 2.2.10:
Compositions of bit slices may be reduced by means of the following.
PROOF: By Lemma 2.2.16,
David Russinoff 2017-08-01