proposition: Lemma lconc_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_A (union_disj q1 q2) (map injgauche qd1) (map injdroite qa2) (union (pont qa1 qd2) (union (injg_d1 q1 d1) (injd_d2 q2 d2)))) (lconc l1 l2).
proof: Proof. intros. unfold eqwordset in |- *. intro w. split. unfold reconnait_A 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. cut (exists x1 : Elt, (exists x2 : Elt, (exists w1 : Word, (exists w2 : Word, dans x1 qa1 /\ dans x2 qd2 /\ chemin (first e1) x1 q1 d1 w1 /\ chemin x2 (first e2) q2 d2 w2 /\ w = Append w1 w2 :>Word)))). 2: apply par_le_pont with qd1 qa2; auto. 2: apply dans_map_trans with qd1; auto. 2: apply automate_def2 with qa1 d1; auto. 2: apply dans_map_trans with qa2; auto. 2: apply automate_def3 with qd2 d2; auto. intros Ht; elim Ht; clear Ht. intros x1 Ht; elim Ht; clear Ht. intros x2 Ht; elim Ht; clear Ht. intros w1 Ht; elim Ht; clear Ht. intros w2 Ht; elim Ht; clear Ht. intros H7 Ht; elim Ht; clear Ht. intros H8 Ht; elim Ht; clear Ht. intros H9 Ht; elim Ht; clear Ht. intros H10 H11. unfold lconc in |- *. exists w1. exists w2. split. unfold eqwordset in H0; elim (H0 w1). intros. apply H12. unfold reconnait in |- *. split. apply Append_inmonoid_g with w2. rewrite <- H11; auto. exists (first e1). exists x1. split; auto. apply dans_map_injg; auto. split. unfold eqwordset in H2; elim (H2 w2). intros. apply H12. unfold reconnait in |- *. split. apply Append_inmonoid_d with w1. rewrite <- H11; auto. exists x2. exists (first e2). split; auto. split; [ apply dans_map_injd; auto | auto ]. assumption. unfold lconc in |- *. intro Ht; elim Ht; clear Ht. intros w1 Ht; elim Ht; clear Ht. intros w2 Ht; elim Ht; clear Ht. intros H3 Ht; elim Ht; clear Ht. intros H4 H5. cut (reconnait q1 qd1 qa1 d1 w1). 2: unfold eqwordset in H0. 2: elim (H0 w1); intros. 2: auto. intro H6. cut (reconnait q2 qd2 qa2 d2 w2). 2: unfold eqwordset in H2. 2: elim (H2 w2); intros. 2: auto. intro H7. rewrite H5. elim H6. intros H8 Ht; elim Ht; clear Ht; intros e1 Ht; elim Ht; clear Ht; intros x1 Ht; elim Ht; clear Ht; intros H9 Ht; elim Ht; clear Ht; intros H10 H11. elim H7. intros H12 Ht; elim Ht; clear Ht; intros x2 Ht; elim Ht; clear Ht; intros e2 Ht; elim Ht; clear Ht; intros H13 Ht; elim Ht; clear Ht; intros H14 H15. unfold reconnait_A in |- *. split. apply inmonoid_Append; auto. exists (couple e1 zero). exists (couple e2 un). split. replace (couple e1 zero) with (injgauche e1); auto. split. replace (couple e2 un) with (injdroite e2); auto. apply reconnait_Append with qd1 qa2 x1 x2; auto. Qed.
imports: Ensf Max Words Dec Reg Rat