English
The bitwise difference with and with not yields bit with and-not parity: ldiff (bit a m) (bit b n) = bit (a ∧ ¬b) (ldiff m n).
Русский
Побитовая разность через и с не равно bit (a ∧ ¬b) (ldiff m n).
LaTeX
$$$$ \operatorname{ldiff\_{bit}}(a,m,b,n) = \operatorname{bit}(a \land \lnot b)(\operatorname{ldiff} m n). $$$$
Lean4
@[simp]
theorem ldiff_bit (a m b n) : ldiff (bit a m) (bit b n) = bit (a && not b) (ldiff m n) := by
rw [← bitwise_diff, bitwise_bit]