proposition: Theorem nfa2_to_dfa : { A : dfa char | dfa_lang A =i nfa2_lang M & #|A| <= 2 ^ (#|M| ^ 2 + #|M|) }.
proof: Proof. exists (classifier_to_dfa (nfa2_to_classifier)); first exact: classifier_to_dfa_correct. rewrite card_sub (leqRW (max_card _)) [#|_|]/=. by rewrite card_prod expnD mulnC leq_mul //= card_set // card_prod -mulnn. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)