proposition: Lemma nfa_for_exE n (A : nfa (vec n.+1)) w : w \in nfa_lang (nfa_for_ex A) -> exists b : seq bool, glue b w \in nfa_lang A.
proof: Proof. rewrite /nfa_lang /= !inE => H. suff S (q:A) : @nfa_accept _ (nfa_for_ex A) q w -> exists b, nfa_accept q (glue b w). { case/exists_inP : H => p p1 /S [b b1]. exists b. rewrite inE. by apply/exists_inP; exists p. } elim: w q {H} => [|v vs IH] q /=. - rewrite inE => /exists_inP [f f1 /connectP[p]]. elim: p q => [x _ |p ps IHp q /= /andP [pth1 pth2]] /= E; first by exists nil; subst. case: (IHp _ pth2 E) => bs Hbs. case/existsP : pth1 => b pth1. exists (b::bs). by apply/exists_inP; exists p. - case/exists_inP => p /= /existsP [b p1] p2. case: (IH _ p2) => bs Hbs. exists (b::bs). by apply/exists_inP; exists p. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)