proposition: Lemma lunion_is_reg1 : forall (q1 qd1 qa1 d1 q2 qd2 qa2 d2 : Ensf) (l1 l2 : wordset), automate q1 qd1 qa1 d1 -> eqwordset (reconnait q1 qd1 qa1 d1) l1 -> automate q2 qd2 qa2 d2 -> eqwordset (reconnait q2 qd2 qa2 d2) l2 -> eqwordset (reconnait (union_disj q1 q2) (union_disj qd1 qd2) (union_disj qa1 qa2) (union (injg_d1 q1 d1) (injd_d2 q2 d2))) (lunion l1 l2).
proof: Proof. intros. unfold eqwordset in |- *. intro w. split. unfold reconnait in |- *. intro Ht; elim Ht; clear Ht. intros H3 Ht; elim Ht; clear Ht. intros e1 Ht; elim Ht; clear Ht. intros e2 Ht; elim Ht; clear Ht. intros H4 Ht; elim Ht; clear Ht. intros H5 H6. unfold union_disj in H4. cut (dans e1 (map injgauche qd1) \/ dans e1 (map injdroite qd2)); auto. intro Ht; elim Ht; clear Ht. intro H7. unfold lunion in |- *. left. cut (chemin (first e1) (first e2) q1 d1 w /\ dans e2 (map injgauche qa1)). 2: apply chemin_restriction_1 with qd1 q2 qa2 d2; auto. 2: cut (inclus qd1 q1). 3: apply automate_def2 with qa1 d1; auto. 2: intro; apply dans_map_trans with qd1; auto. intro Ht; elim Ht; clear Ht; intros H8 H9. unfold eqwordset in H0. elim (H0 w). intros H10 H11. apply H10. unfold reconnait in |- *. split; auto. exists (first e1). exists (first e2). split. apply dans_map_injg; auto. split. apply dans_map_injg; auto. assumption. intro H7. unfold lunion in |- *. right. cut (chemin (first e1) (first e2) q2 d2 w /\ dans e2 (map injdroite qa2)). 2: apply chemin_restriction_2 with qd2 q1 qa1 d1; auto. 2: cut (inclus qd2 q2). 3: apply automate_def2 with qa2 d2; auto. 2: intro; apply dans_map_trans with qd2; auto. intro Ht; elim Ht; clear Ht; intros H8 H9. unfold eqwordset in H2. elim (H2 w). intros H10 H11. apply H10. unfold reconnait in |- *. split; auto. exists (first e1). exists (first e2). split. apply dans_map_injd; auto. split. apply dans_map_injd; auto. assumption. unfold lunion in |- *. intro Ht; elim Ht; clear Ht. intro H3. unfold eqwordset in H0. elim (H0 w). intros H4 H5. cut (reconnait q1 qd1 qa1 d1 w); auto. intro Ht; elim Ht; clear Ht. intros H6 Ht; elim Ht; clear Ht. intros e1 Ht; elim Ht; clear Ht. intros e2 Ht; elim Ht; clear Ht. intros H7 Ht; elim Ht; clear Ht. intros H8 H9. unfold reconnait in |- *. split; auto. exists (couple e1 zero). exists (couple e2 zero). split. unfold union_disj in |- *. apply union_g. replace (couple e1 zero) with (injgauche e1); auto. split. unfold union_disj in |- *. apply union_g. replace (couple e2 zero) with (injgauche e2); auto. apply chemin_extension_1 with qd1 qa1; auto. apply dans_trans with qd1; auto. apply automate_def2 with qa1 d1; auto. intro H3. unfold eqwordset in H2. elim (H2 w). intros H4 H5. cut (reconnait q2 qd2 qa2 d2 w); auto. intro Ht; elim Ht; clear Ht. intros H6 Ht; elim Ht; clear Ht. intros e1 Ht; elim Ht; clear Ht. intros e2 Ht; elim Ht; clear Ht. intros H7 Ht; elim Ht; clear Ht. intros H8 H9. unfold reconnait in |- *. split; auto. exists (couple e1 un). exists (couple e2 un). split. unfold union_disj in |- *. apply union_d. replace (couple e1 un) with (injdroite e1); auto. split. unfold union_disj in |- *. apply union_d. replace (couple e2 un) with (injdroite e2); auto. apply chemin_extension_2 with qd2 qa2; auto. apply dans_trans with qd2; auto. apply automate_def2 with qa2 d2; auto. Qed.
imports: Ensf Max Words Dec Reg Rat