English
If n ≠ 0, m ≠ 0, then bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n/2) (m/2)).
Русский
Если n ≠ 0 и m ≠ 0, то bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n/2) (m/2)).
LaTeX
$$$$ \\text{Если } n \\neq 0 \\text{ и } m \\neq 0, \\quad \\mathrm{bitwise}\\; f\\; n\\; m = \\mathrm{bit}\\bigl( f(\\mathrm{bodd}\\, n)(\\mathrm{bodd}\\, m) \\bigr) (\\mathrm{bitwise}\\; f (n/2) (m/2)) $$$$
Lean4
theorem bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n / 2) (m / 2)) :=
by
conv_lhs => unfold bitwise
have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by simp only [mod_two_of_bodd]; cases bodd x <;> rfl
simp only [hn, hm, mod_two_iff_bod, ite_false, bit, two_mul, Bool.cond_eq_ite]
