fact: Definition nfa_to_dfa := {| dfa_s := nfa_s A; dfa_fin := [set X | X :&: nfa_fin A != set0]; dfa_trans X a := [set q | [exists (p | p \in X), nfa_trans p a q]] |}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)