is_regular_symm_diff
theoremverified
The symmetric difference of two regular languages is regular.
Statement
theorem is_regular_symm_diff {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (symmDiff L1 L2).IsRegular
- Source
- Hopcroft, Motwani & Ullman, Exercise 4.2
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- is_regular_diffThe difference L1 \\ L2 of two regular languages is regular.
Read back from the Lean
For any type α and any languages L1, L2 : Language α, if L1 is regular and L2 is regular, then their symmetric difference symmDiff L1 L2 is also regular.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- The symmetric difference of two regular languages is regular. -/ theorem is_regular_symm_diff {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (symmDiff L1 L2).IsRegular := by rw [symmDiff_def] exact (is_regular_diff h1 h2).add (is_regular_diff h2 h1)