The binary functions *logand*, *logior*, and *logxor* are ACL2
primitives. The “definitions” presented below are actually formalized as theorems derived from ACL2 axioms.

It is not obvious that Definition 3.1.1 is an admissible recursive definition.
In order to establish that it is satisfied by a unique function, it will suffice to demonstrate
the existence of a *measure* function
that strictly decreases on each recursive call. Thus, we define

(1) .

(2) .

Since the restrictions imply that at least one of and is neither 0 nor -1, (1) follows from Lemma 1.1.6. To establish (2), note that either , , or . In any case,

Precisely the same argument applies to the following two definitions.

Notation: We adopt the following standard notation:

;

;

.

PROOF: We may assume that , , and . Thus,

PROOF: By Lemma 3.1.1,

PROOF: The same argument applies to both operations. The claim is trivial if , , , or . In all other cases, and are -bit vectors and by induction, so is, for example, . Thus,

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that , , , and .
By Definition 3.1.1 and Lemma 1.2.18,

By Lemma 1.2.22, induction, Lemma 2.2.4, and Lemma 2.2.17, the first addend my be written as

and by Lemmas 2.3.2 and 2.3.16, the second addend is

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that , , , and .
By Lemma 1.1.5, induction, and Definition 3.1.1,

For all , , , , , and ,

*(a)
----
=
----
*

*(b)
----
=
----
*

*(c)
----
=
----
*

PROOF: We present the proof for (a); (b) and (c) are similar.

Let
----.
By Lemmas 3.1.4 and 2.4.13,

------ | |||

-- |

By Lemma 3.1.5,

----

where, by Definition 2.4.1 and the properties of the floor,
-- | -- | ||

-- | |||

- |

Thus,

--

Finally, by Definitions 1.2.1 and 2.4.1,
---- | |||

---- |

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that , , , and .
By induction and Definition 3.1.1,

PROOF:

(a) The claim is trivial if , , or ; otherwise, by Definition 3.1.1, induction, and Lemma 1.1.5,

(b) Similarly,

where, by Lemmas 2.2.4 and 2.2.16,

(c) is similar to (b).

PROOF: By Lemmas 3.1.8 and 1.2.6 and Definition 3.1.2,

PROOF: By Definition 2.0.1 and Lemmas 3.1.4, 3.1.6, and 2.3.17,

By Lemma 3.1.5,

The logical “and” operator may be used to extract a bit slice:

PROOF: The proof is by induction on . If , then and

In the remaining case, and

PROOF: By Lemma 3.1.11,

All three binary logical operators commute with the bit slice operator:

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that , , , and .
By Definition 2.0.1 and Lemmas 3.1.4 and 3.1.5,

Notation: If and are expressions of sizes and , respectively, then we define the size of each of the expressions , , and to be . As a consequence of Lemma 3.1.2, it remains true that if is any expression of size , then the value of is a bit vector of width .

Thus, for example, by Lemma 3.1.13,

David Russinoff 2017-08-01