Bitwise operations on natural numbers #
In the first half of this file, we provide theorems for reasoning about natural numbers from their
bitwise properties. In the second half of this file, we show properties of the bitwise operations
lxor, which are defined in core.
Main results #
eq_of_test_bit_eq: two natural numbers are equal if they have equal bits at every position.
n ≠ 0, then there is some position
ithat contains the most significant
mare numbers and
iis a position such that the
i-th bit of of
nis zero, the
i-th bit of
mis one, and all more significant bits are equal, then
n < m.
Future work #
There is another way to express bitwise properties of natural number:
digits 2. The two ways
should be connected.
bitwise, and, or, xor