proposition: Lemma sat_accept (Ns : n.-tuple (seq nat)) m I : cat Ns (cons [:: m] I) |= accept n <-> exists2 q, q \in nfa_fin A & m \in tnth Ns (rank q).
proof: Proof. split. - case/sat_orE => q. rewrite mem_enum /= cat_size ?cat_prefix // -tnth_nth. move => B /sub1P C. by exists q. - case => q q1 q2. apply: (sat_orI (x := q)); first by rewrite mem_enum. rewrite /= cat_size ?cat_prefix // -tnth_nth. exact/sub1P. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)