English
For all f, a, m, b, n, bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n).
Русский
Для любого f, a, m, b, n: bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n).
LaTeX
$$$$ \operatorname{bitwise} f (\operatorname{bit} a m) (\operatorname{bit} b n) = \operatorname{bit} (f a b) (\operatorname{bitwise} f m n). $$$$
Lean4
@[simp]
theorem bitwise_bit (f : Bool → Bool → Bool) (a m b n) : bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) :=
by
rcases m with m | m <;> rcases n with n | n <;>
simp [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, bit_negSucc]
· by_cases h : f false false <;> simp +decide [h]
· by_cases h : f false true <;> simp +decide [h]
· by_cases h : f true false <;> simp +decide [h]
· by_cases h : f true true <;> simp +decide [h]
