fact: Definition enfa_conc : enfa := {| enfa_s := inl @: nfa_s A1; enfa_f := inr @: nfa_fin A2; enfa_trans c p q := match c,p,q with | Some a,inl p',inl q' => nfa_trans p' a q' | Some a,inr p',inr q' => nfa_trans p' a q' | None,inl p', inr q' => (p' \in nfa_fin A1) && (q' \in nfa_s A2) | _,_,_ => false end |}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)