proposition: Lemma reconnait_Append : forall (q1 qd1 qa1 d1 q2 qd2 qa2 d2 : Ensf) (w2 : Word) (x1 x2 e2 : Elt) (w1 : Word) (e1 : Elt), automate q1 qd1 qa1 d1 -> automate q2 qd2 qa2 d2 -> chemin e1 x1 q1 d1 w1 -> dans x1 qa1 -> chemin x2 e2 q2 d2 w2 -> dans x2 qd2 -> dans e2 qa2 -> chemin_A (union_disj q1 q2) (union (pont qa1 qd2) (union (injg_d1 q1 d1) (injd_d2 q2 d2))) (couple e1 zero) (couple e2 un) (Append w1 w2).
proof: Proof. intros q1 qd1 qa1 d1 q2 qd2 qa2 d2 w2 x1 x2 e2. simple induction w1. intros e1 H_aut1 H_aut2 H H0 H1 H2 H3. cut (Chemin e1 x1 q1 d1 nil); auto. intro H4. cut (dans e1 q1 /\ e1 = x1 :>Elt); auto. intro Ht; elim Ht; clear Ht; intros H5 H6. replace (Append nil w2) with w2; auto. apply chemin_A_epsilon with (couple x2 un). apply chemin_A_d1_d2 with (union (injg_d1 q1 d1) (injd_d2 q2 d2)); auto. apply chemin_chemin_A. apply chemin_extension_2 with qd2 qa2; auto. apply dans_trans with qd2; auto. apply automate_def2 with qa2 d2; auto. replace (couple e1 zero) with (injgauche e1); auto. unfold union_disj in |- *. apply union_g. apply dans_map_inv; auto. apply union_g. unfold pont in |- *. rewrite H6. replace (couple (couple x1 zero) (couple epsilon (couple x2 un))) with (transition_pont (couple x1 x2)); auto. intros x w H e1 H0 H1 H2 H3 H4 H5 H6. replace (Append (cons x w) w2) with (cons x (Append w w2)); auto. cut (Chemin e1 x1 q1 d1 (cons x w)); auto. intro H7. cut (exists e : Elt, chemin e x1 q1 d1 w /\ dans e1 q1 /\ dans x alph /\ dans (couple e1 (couple x e)) d1); auto. intro Ht; elim Ht; clear Ht; intros e Ht; elim Ht; clear Ht; intros H8 Ht; elim Ht; clear Ht; intros H9 Ht; elim Ht; clear Ht; intros H10 H11. apply chemin_A_cons with (couple e zero); auto. unfold union_disj in |- *. apply union_g. replace (couple e1 zero) with (injgauche e1); auto. apply union_d. apply union_g. unfold injg_d1 in |- *. apply imp_dans_tq; auto. apply coupl2_inv. replace (couple e1 zero) with (injgauche e1); auto. apply coupl2_inv; auto. replace (couple e zero) with (injgauche e); auto. apply dans_map_inv; auto. apply dans_e1_q with d1 w x1; auto. Qed.
imports: Ensf Max Words Dec Reg Rat