proposition: Lemma enfaE x p : (enfa_accept p x) <-> (exists2 q : nfa_of, q \in eps_reach p & nfa_accept q x).
proof: Proof. split. - elim => {p x} [q H|p a q x H _ [q' Hq1 Hq2]|p p' x]. + exists q => //. by rewrite inE connect0. + exists p => /=; first by rewrite inE connect0. apply/exists_inP. exists q' => //. apply/exists_inP. by exists q. + move => H1 H2 [q Hq1 Hq2]. exists q => //. rewrite !inE in Hq1 *. exact: connect_trans (connect1 _) Hq1. - elim: x p => [|a x IH] p [p'] R /= H. apply: lift_accept R _. exact: EnfaFin. case/exists_inP : H => q /exists_inP [q' pq' qq'] H. apply: lift_accept R _. apply: EnfaSome pq' _. apply: IH. by exists q. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)