proposition: Lemma sat_run (Ns : n.-tuple (seq nat)) m I : cat Ns (cons [:: m] I) |= run n <-> (forall k, k < m -> exists (p:A) (a:T) (q:A), nfa_trans p a q /\ k \in I (rank a) /\ k \in tnth Ns (rank p) /\ k.+1 \in tnth Ns (rank q)).
proof: Proof. split. - move => H k lt_m. move/sat_all1/(_ k.+1) : H. move/sat_all1/(_ k). rewrite 2!sat_imp. case/(_ _ _)/Wrap. + by apply/(sat_succ (x := k) (y := k.+1)). + move => /= ? y /seq1P ->. rewrite cat_beyond // subnn /=. by move/seq1P->. + case/sat_orE => [[[p a] q]]. rewrite mem_enum inE /= => B. rewrite !sat_and. (do 2 case) => /= /sub1P C /sub1P D /sub1P E. exists p, a, q. repeat split => //. * by rewrite cat_beyond ?leq_addl -?addnBA // subnn addn0 in C. * by rewrite cat_prefix // -tnth_nth in D. * by rewrite cat_prefix // -tnth_nth in E. - move => H. apply/sat_all1 => k'. apply/sat_all1 => k. rewrite !sat_imp => B C. move/sat_succ : B => /(_ k' k). case/(_ _ _)/Wrap => // ?;subst. case: (H _ (C k m _ _)); rewrite /= ?cat_size /= ?mem_head //. move => p [a] [q] [paq [D [E F]]]. apply: (sat_orI (x := (p,a,q))); first by rewrite mem_enum. rewrite !sat_and; repeat split. + apply/sub1P. rewrite /= cat_beyond ?leq_addl //. by rewrite -addnBA // subnn addn0. + apply/sub1P. by rewrite /= cat_prefix // -tnth_nth. + apply/sub1P. by rewrite /= cat_prefix // -tnth_nth. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)