proposition: Lemma dfa2Pn x : reflect (exists T, @reject_cert x T) (x \notin nfa2_lang M).
proof: Proof. apply: introP => [H|]. - exists (run_table x) ; split; first by rewrite inE ?connect0. + apply/pred0P => q. rewrite !inE. apply: contraNF H => C. by apply/existsP; exists q. + move => i p j q. rewrite !inE => ? S. exact: connect_trans (connect1 S). - move/negPn => /exists_inP [q Hq1 Hq2] [c C]. have/(sub_run C) H : q \in run_table x ord_max by rewrite inE. case: C => _ /disjoint_setI0 C _. move: C. move/setP/(_ q). by rewrite !inE Hq1 H. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages nfa two_way)