fact: Record deterministic (M : nfa2 char) : Prop := { detC : forall (p:M) a, #|nfa2_trans p a| <= 1; detL : forall (p:M), #|nfa2_transL p| <= 1; detR : forall (p:M), #|nfa2_transR p| <= 1}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)