English
For any binary Boolean operation f, bitwise (swap f) equals swap (bitwise f).
Русский
Для любой булевой бинарной функции f верно, что bitwise (swap f) = swap (bitwise f).
LaTeX
$$$ bitwise(\text{Function.swap } f) = \text{Function.swap}(bitwise f) $$$
Lean4
theorem bitwise_swap {f : Bool → Bool → Bool} : bitwise (Function.swap f) = Function.swap (bitwise f) :=
by
funext m n
simp only [Function.swap]
induction m using Nat.strongRecOn generalizing n with
| ind m ih => ?_
rcases m with - | m <;> rcases n with - | n <;> try rw [bitwise_zero_left, bitwise_zero_right]
· specialize ih ((m + 1) / 2) (div_lt_self' ..)
simp [bitwise_of_ne_zero, ih]
