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