proposition: Lemma chemin_extension_1 : forall (q1 qd1 qa1 d1 q2 d2 : Ensf) (w : Word) (e1 e2 : Elt), automate q1 qd1 qa1 d1 -> chemin e1 e2 q1 d1 w -> dans e1 q1 -> dans e2 qa1 -> chemin (couple e1 zero) (couple e2 zero) (union_disj q1 q2) (union (injg_d1 q1 d1) (injd_d2 q2 d2)) w.
proof: Proof. intros q1 qd1 qa1 d1 q2 d2. simple induction w. intros e1 e2 H_aut. intros. cut (Chemin e1 e2 q1 d1 nil); auto. intro. cut (dans e1 q1 /\ e1 = e2 :>Elt); auto. intro Ht; elim Ht; clear Ht. intros H3 H4. apply chemin_nil; auto. unfold union_disj in |- *. apply union_g. replace (couple e1 zero) with (injgauche e1); auto. rewrite H4; auto. intros x w0 H e1 e2 H_aut. intros. cut (Chemin e1 e2 q1 d1 (cons x w0)); auto. intro. cut (exists e : Elt, chemin e e2 q1 d1 w0 /\ 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 H4 Ht; elim Ht; clear Ht. intros H5 Ht; elim Ht; clear Ht. intros H6 H7. cut (dans e q1). intro dans_e_q1. 2: cut (inclus d1 (prodcart q1 (prodcart alph q1))). 3: apply automate_def1 with qd1 qa1; auto. 2: intro. 2: cut (dans (couple e1 (couple x e)) (prodcart q1 (prodcart alph q1))). 3: apply dans_trans with d1; auto. 2: intro. 2: cut (dans e1 q1 /\ dans (couple x e) (prodcart alph q1)). 3: apply coupl2; auto. 2: intro Ht; elim Ht; clear Ht. 2: intros H10 H11. 2: cut (dans x alph /\ dans e q1). 3: apply coupl2; auto. 2: intro Ht; elim Ht; clear Ht. 2: auto. apply chemin_cons with (couple e zero); auto. unfold union_disj in |- *. apply union_g. replace (couple e1 zero) with (injgauche e1); auto. 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. Qed.
imports: Ensf Max Words Dec Reg Rat