2.2 Bit Slices

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: .

PROOF: By Lemma 1.2.21, .

If the lower limit of a bit slice is 0, it reduces to a call to :

PROOF:

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*.

*(a)
;*

*(b)
;*

*(c)
.*

PROOF: By Definition 2.0.1 and Lemmas 1.2.18 and 1.2.20,

The other results follow similarly from Lemmas 1.2.19 and 1.2.23.

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.

PROOF: Since
,
. Applying
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,

If , then by Definition 2.0.1 and Corollary 1.2.9,

0 |

and by Lemma 2.2.13.

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,

If , then this reduces, by Corollary 1.2.21, to

David Russinoff 2017-08-01