proposition: Lemma chemin_A_g0_e2 : forall (q qd qa d : Ensf) (g0 e1 e2 : Elt) (w : Word), automate q qd qa d -> ~ dans g0 q -> chemin_A (add g0 q) (union d (delta_D g0 qd)) e1 e2 w -> e1 = g0 :>Elt -> dans e2 qa -> exists e : Elt, dans e qd /\ chemin_A (add g0 q) (union d (delta_D g0 qd)) e e2 w.
proof: Proof. intros q qd qa d g0 e1 e2 w H_aut H_g0 H. elim H; clear H. intros e0 e3 H H0 H1 H2. absurd (dans g0 q); auto. rewrite <- H1. rewrite H0. apply dans_trans with qa; auto. apply automate_def3 with qd d; auto. intros e0 e e3 x w0 H H0 H1 H2 H3 H4 H5. clear H0. cut (dans (couple e0 (couple x e)) d \/ dans (couple e0 (couple x e)) (delta_D g0 qd)); auto. intro Ht; elim Ht; clear Ht. intro. cut (dans (couple e0 (couple x e)) (prodcart q (prodcart alph q))). 2: apply dans_trans with d; auto. 2: apply automate_def1 with qd qa; auto. intro. cut (dans e0 q /\ dans (couple x e) (prodcart alph q)). 2: apply coupl2; auto. intro Ht; elim Ht; clear Ht; intros. absurd (dans g0 q); auto. rewrite <- H4. assumption. unfold delta_D in |- *. intro. cut (exists y : Elt, dans y qd /\ couple e0 (couple x e) = transition_D g0 y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht; intros y' Ht; elim Ht; clear Ht; intros. unfold transition_D in H7. cut (e0 = g0 :>Elt /\ couple x e = couple epsilon y' :>Elt). 2: apply equal_couple; auto. intro Ht; elim Ht; clear Ht; intros. cut (x = epsilon :>Elt /\ e = y' :>Elt). 2: apply equal_couple; auto. intro Ht; elim Ht; clear Ht; intros. absurd (dans x alph); auto. rewrite H10. red in |- *; intro; apply not_dans_epsilon_alph; assumption. intros e0 e e3 w0 H H0 H1 H2 H3 H4. clear H0. exists e. split. 2: assumption. cut (dans (couple e0 (couple epsilon e)) d \/ dans (couple e0 (couple epsilon e)) (delta_D g0 qd)); auto. intro Ht; elim Ht; clear Ht. intro. cut (dans (couple e0 (couple epsilon e)) (prodcart q (prodcart alph q))). 2: apply dans_trans with d; auto. 2: apply automate_def1 with qd qa; auto. intro. cut (dans e0 q /\ dans (couple epsilon e) (prodcart alph q)). 2: apply coupl2; auto. intro Ht; elim Ht; clear Ht; intros. cut (dans epsilon alph /\ dans e q). 2: apply coupl2; auto. intro Ht; elim Ht; clear Ht; intros. absurd (dans epsilon alph); auto. red in |- *; intro; apply not_dans_epsilon_alph; assumption. unfold delta_D in |- *. intro. cut (exists y : Elt, dans y qd /\ couple e0 (couple epsilon e) = transition_D g0 y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht; intros y' Ht; elim Ht; clear Ht; intros. unfold transition_D in H6. cut (e0 = g0 :>Elt /\ couple epsilon e = couple epsilon y' :>Elt). 2: apply equal_couple; auto. intro Ht; elim Ht; clear Ht; intros. cut (epsilon = epsilon :>Elt /\ e = y' :>Elt). 2: apply equal_couple; auto. intro Ht; elim Ht; clear Ht; intros. rewrite H10. assumption. Qed.
imports: Ensf Max Words Dec