Lemmas about bitwise operations on natural numbers. #
Possibly only of archaeological significance.
shiftLeft' b m n performs a left shift of
and adds the bit
b as the least significant bit each time.
Returns the corresponding natural number
A recursion principle for
bit representations of natural numbers.
For a predicate
C : Nat → Sort*, if instances can be
constructed for natural numbers of the form
bit b n,
they can be constructed for all natural numbers.
- One or more equations did not get rendered due to their size.