Commit 2025-05-19 15:46 70816aec

feat(Computability): regular languages are closed under reversal (#21573) This PR proves that regular languages are closed under reversal. It works by reversing the transitions in the NFA, and proving that the resulting automaton matches the reversed language. The argument proceeds by induction on the input word, ensuring that, at each character, the state sets for the forward and reverse automaton correspond to each other. I also clean up the existing NFA module, which includes making the M argument implicit by default. I can revert that if it's controversial. Thank you @Rob23oba for their help with the induction proof.