proposition: Lemma par_le_pont : forall (q1 qd1 qa1 d1 q2 qd2 qa2 d2 : Ensf) (e1 e2 : Elt) (w : Word), automate q1 qd1 qa1 d1 -> automate q2 qd2 qa2 d2 -> chemin_A (union_disj q1 q2) (union (pont qa1 qd2) (union (injg_d1 q1 d1) (injd_d2 q2 d2))) e1 e2 w -> dans e1 (map injgauche q1) -> dans e2 (map injdroite q2) -> 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))).
proof: Proof. intros q1 qd1 qa1 d1 q2 qd2 qa2 d2 e1 e2 w H_aut1 H_aut2 H. elim H. intros e0 e3 H0 H1 H2 H3. absurd (dans e3 (map injdroite q2)); auto. apply absurd_injg_injd with q1. rewrite <- H1; assumption. intros e0 e e3 x w0 H0 H1 H2 H3 H4 H5 H6. cut (dans e (map injgauche q1)). 2: apply transition_a_gauche with qa1 d1 q2 qd2 d2 e0 x; auto. intro H7. elim (H1 H7 H6); clear H1. 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 H8 Ht; elim Ht; clear Ht; intros H9 Ht; elim Ht; clear Ht; intros H10 Ht; elim Ht; clear Ht; intros H11 H12. exists x1. exists x2. exists (cons x w1'). exists w2. split; [ assumption | split; [ assumption | split ] ]. 2: split. 2: assumption. 2: rewrite H12; auto. apply chemin_cons with (first e); auto. apply dans_map_injg; auto. apply transition_a_gauche_2 with q1 qa1 q2 qd2 d2; auto. intros e0 e e3 w0 H0 H1 H2 H3 H4 H5. clear H1. exists (first e0). exists (first e). exists nil. exists w0. cut (dans e0 (map injgauche qa1) /\ dans e (map injdroite qd2)). 2: apply transition_dans_pont with q1 d1 q2 d2; auto. intro Ht; elim Ht; clear Ht; intros H6 H7. split; [ apply dans_map_injg; assumption | split ]. apply dans_map_injd; assumption. split. apply chemin_nil; auto. apply dans_trans with qa1. apply dans_map_injg; auto. apply automate_def3 with qd1 d1; auto. split; auto. apply chemin_A_chemin_2 with q1 qa1 d1 qd2; auto. apply dans_map_trans with qd2; auto. apply automate_def2 with qa2 d2; auto. Qed.
imports: Ensf Max Words Dec Reg Rat