proposition: Lemma coincidence I I' s: agree (bound s) I I' -> satisfies I s <-> satisfies I' s.
proof: Proof. elim: s I I' => [X Y|X Y||s IHs t IHt|s IHs] /= I I' C. - split. + move => A B. rewrite -!C ?leq_maxl ?leq_maxr //. exact: A. + move => A B. rewrite !C ?leq_maxl ?leq_maxr //. exact: A. - split => H x y;[rewrite -!C|rewrite !C]; try solve [exact: H|by rewrite ?leq_maxl ?leq_maxr]. - tauto. - by rewrite -(IHs I I') ?(IHt I I') //; apply: agree_dc C; rewrite ?leq_maxl ?leq_maxr. - have bound_s N : agree (bound s) (cons N I) (cons N I'). { move => X. case: X C => //= Y A B. apply: A. rewrite -ltnS. by case: (bound s) B. } split. + move => [N] sat_s. exists N. rewrite -IHs; [exact: sat_s | exact: bound_s]. + move => [N] sat_s. exists N. rewrite IHs; [exact: sat_s | exact: bound_s]. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)