proposition: Lemma sat_max (w : word T) m : cons [:: m] (I_of (vec_of w)) |= max <-> m = size w.
proof: Proof. split. - move/sat_all1 => B. apply/eqP. rewrite eqn_leq [_ <= m]leqNgt [m <= _]leqNgt. apply/andP; split; apply/negP => C. + case: m C B => // m C /(_ m). case/sat_and => [/sat_imp B _]. move: B. case/(_ _)/Wrap; first by move => ? ? /seq1P-> /seq1P->. case/sat_orE => a _ /= /sub1P /I_of_vev_max => D. rewrite ltnS in C. move: (leq_trans D C). by rewrite ltnn. + move/(_ m) : B. case/sat_and => _. move/sat_imp. case/(_ _)/Wrap. * set a := (tnth (in_tuple w) (Ordinal C)). apply: (sat_orI (x := a)); first by rewrite mem_enum. apply/sub1P => /=. by rewrite I_of_vecP // {2}/a (tnth_nth a). * move/(_ m m) => /=. rewrite !mem_head ltnn. by case/(_ _ _)/Wrap. - move->. rewrite sat_all1 => k. rewrite sat_and; split. + rewrite /= => H. move: H => /(_ k (size w) (mem_head _ _) (mem_head _ _)) => H. pose a0 := tnth (in_tuple w) (Ordinal H). apply (sat_orI (x := nth a0 w k)); first by rewrite mem_enum. rewrite /= => ? /seq1P->. by rewrite I_of_vecP ?(set_nth_default a0). + case/sat_orE => a _ /sub1P /=. rewrite /vec_of /I_of mem_filter => /andP [_]. by rewrite mem_iota add0n size_map /= => H ? ? /seq1P-> /seq1P->. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)