proposition: Lemma runI x s r : size r = size x -> last s r \in nfa_fin M -> (forall i : 'I_(size x), nth s (s::r) i.+1 \in nfa_trans (nth s (s::r) i) (tnth (in_tuple x) i)) -> nfa_run x s r.
proof: Proof. elim: x s r => [|a x IHx ] s r /=. - move/eqP => e inF _. rewrite size_eq0 in e. rewrite (eqP e) in inF *. exact: run0. - case: r => // p r /eqP /=. rewrite eqSS => /eqP R1 R2 I. apply: runS (I ord0) _ => /=. apply: IHx => // i. move: (I (inord i.+1)). rewrite /tnth /= !inordK /= ?ltnS //. rewrite !(set_nth_default p) /= ?R1 // 1?ltnW ?ltnS //. by rewrite -[x]/(val (in_tuple x)) -!tnth_nth. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)