fact: Record nfa2 := Nfa2 { nfa2_state :> finType; nfa2_s : nfa2_state; nfa2_f : {set nfa2_state}; nfa2_trans : nfa2_state -> char -> {set nfa2_state * dir}; nfa2_transL : nfa2_state -> {set nfa2_state}; nfa2_transR : nfa2_state -> {set nfa2_state}}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)