ldiff_bit — Mathlib

English

The left-difference of bits distributes: ldiff (bit a m) (bit b n) = bit (a ∧ ¬b) (ldiff m n).

Русский

Левосторонняя разность битов распадается: ldiff (bit a m) (bit b n) = bit (a ∧ ¬b) (ldiff m n).

LaTeX

$$$$ \\mathrm{ldiff}\\; (\\mathrm{bit}\\ a\\ m) (\\mathrm{bit}\\ b\\ n) = \\mathrm{bit}\\ (a \\land \\lnot b)\\ (\\mathrm{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) :=
  bitwise_bit

Похожие утверждения