Nat.testBit_bitwise
theorem Nat.testBit_bitwise :
∀ {f : Bool → Bool → Bool},
f false false = false → ∀ (x y i : ℕ), (Nat.bitwise f x y).testBit i = f (x.testBit i) (y.testBit i)
This theorem states that for any boolean function `f`, given that `f` returns false when both its arguments are false, and for any natural numbers `x`, `y`, and `i`, the `(i+1)` least significant bit of the bitwise operation `f` applied to `x` and `y` is equal to the function `f` applied to the `(i+1)` least significant bits of `x` and `y`. In simple terms, it says that the `(i+1)` least significant bit of the result of a bitwise operation on two numbers is determined by applying the operation to the `(i+1)` least significant bits of the two numbers.
More concisely: For any boolean function `f` with the property that `f(false, false) = false, and for all natural numbers `x`, `y`, the `(i+1)`-th bit of the bitwise operation `f(x ⊔ y)` is equal to `f(x(i) ⊔ y(i))`, where `x(i)` and `y(i)` are the `(i+1)`-th bits of `x` and `y`, respectively.
|
Nat.testBit_and
theorem Nat.testBit_and : ∀ (x y i : ℕ), (x &&& y).testBit i = (x.testBit i && y.testBit i)
The theorem `Nat.testBit_and` states that for all natural numbers `x`, `y`, and `i`, the `i`-th least significant bit of the bitwise AND operation between `x` and `y` is determined by the logical AND operation between the `i`-th least significant bit of `x` and the `i`-th least significant bit of `y`. This means that when comparing the bit representation at a certain position for both `x` and `y`, if both bits are 1, the result will also have 1 in that position; otherwise, it will be 0.
More concisely: For all natural numbers x, y, and i, the i-th bit of x AND y is equal to the logical AND of the i-th bits of x and y.
|
Nat.testBit_to_div_mod
theorem Nat.testBit_to_div_mod : ∀ {i x : ℕ}, x.testBit i = decide (x / 2 ^ i % 2 = 1)
The theorem `Nat.testBit_to_div_mod` states that for any natural numbers `i` and `x`, the `i+1`-th least significant bit of `x` is `1` if and only if the integer division of `x` by `2` to the power `i`, taken modulo `2`, equals `1`. In other words, this bit is determined by the remainder when `x` is divided by `2` to the power `i`.
More concisely: For any natural numbers `i` and `x`, the `i`-th binary digit of `x` is `1` if and only if `x` mod (2 ^ `i`) = 1.
|
Nat.bitwise_lt_two_pow
theorem Nat.bitwise_lt_two_pow :
∀ {x n y : ℕ} {f : Bool → Bool → Bool}, x < 2 ^ n → y < 2 ^ n → Nat.bitwise f x y < 2 ^ n
This theorem, `Nat.bitwise_lt_two_pow`, states that for any natural numbers `x`, `n`, and `y`, and any binary function `f` from booleans to booleans, if `x` and `y` are both less than 2 to the power of `n`, then the bitwise operation `f` applied to `x` and `y` results in a natural number that is also less than 2 to the power of `n`. The bitwise operation is defined as `Nat.bitwise f x y`.
More concisely: For all natural numbers x, y, and n, and binary function f from booleans to booleans, if x < 2^n and y < 2^n then Nat.bitwise f x y < 2^n.
|
Nat.and_one_is_mod
theorem Nat.and_one_is_mod : ∀ (x : ℕ), x &&& 1 = x % 2
This theorem states that for any natural number `x`, the bitwise `and` operation of `x` and `1` is equal to the remainder when `x` is divided by `2`. In other words, it's asserting that performing a bitwise `and` operation on a natural number `x` and `1` will always give the same result as taking modulus `2` of `x`. This is reliable because both operations effectively determine if `x` is odd or even.
More concisely: For any natural number `x`, `x` and `1` bitwise AND equals the remainder of `x` divided by `2`.
|
Nat.zero_testBit
theorem Nat.zero_testBit : ∀ (i : ℕ), Nat.testBit 0 i = false
The theorem `Nat.zero_testBit` states that for any natural number `i`, when we test the `(i+1)`th least significant bit of `0`, the result is `false`. In mathematical terms, this means that in the binary representation of zero, all the bits are `0`. Hence, no matter which bit position you check, the result will be `0`, which in the context of the `Nat.testBit` function, returns `false`.
More concisely: For all natural numbers i, the i-th bit of the binary representation of 0 is 0.
|
Nat.testBit_succ
theorem Nat.testBit_succ : ∀ (x i : ℕ), x.testBit i.succ = (x / 2).testBit i
The theorem `Nat.testBit_succ` states that for any two natural numbers `x` and `i`, the `(i+2)`-th least significant bit of `x` is the same as the `(i+1)`-th least significant bit of `x / 2`. In other words, when we move to the next least significant bit in `x`, it's equivalent to halving `x` and checking the same bit position as before.
More concisely: The `(i+2)`-th least significant bit of a natural number `x` equals the `(i+1)`-th least significant bit of `x / 2`.
|
Nat.eq_of_testBit_eq
theorem Nat.eq_of_testBit_eq : ∀ {x y : ℕ}, (∀ (i : ℕ), x.testBit i = y.testBit i) → x = y
The theorem `Nat.eq_of_testBit_eq` states that for any two natural numbers `x` and `y`, if their respective bits at all positions are equal (as determined by the `Nat.testBit` function), then `x` and `y` are equal. In other words, two natural numbers are deemed equal if their binary representations are the same.
More concisely: If for all i, Nat.testBit x i = Nat.testBit y i, then x = y.
|