English
In a Boolean algebra, the symmetric difference expands to a disjunctive normal form consisting of all triples with certain parity conditions.
Русский
В буловой алгебре симметрическая разность раскладывается в дизъюнктную нормальную форму, включающую все триады с заданными условиями по парности.
LaTeX
$$$a \Delta (b \Delta c) = a \land b \land c \;\lor\; a \land \lnot b \land \lnot c \;\lor\; \lnot a \land b \land \lnot c \;\lor\; \lnot a \land \lnot b \land c.$$$
Lean4
theorem symmDiff_symmDiff_right' : a ∆ (b ∆ c) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c :=
calc
a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ := by {
rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
}
_ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ := by {
rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
}
_ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c :=
(by
congr 1
· congr 1
rw [inf_comm, inf_assoc]
· apply inf_left_right_swap)
