proposition: Lemma transition_par_epsilon : forall (q qa d : Ensf) (g0 e0 e : Elt), automate q (singleton g0) qa d -> dans (couple e0 (couple epsilon e)) (fun_d_dstar g0 qa d) -> dans e0 qa /\ e = g0 :>Elt.
proof: Proof. intros. unfold fun_d_dstar in H0. cut (dans (couple e0 (couple epsilon e)) d \/ dans (couple e0 (couple epsilon e)) (delta g0 qa)); auto. intro Ht; elim Ht; clear Ht. intro. cut (inclus d (prodcart q (prodcart alph q))). 2: apply automate_def1 with (singleton g0) qa; assumption. intro. cut (dans (couple e0 (couple epsilon e)) (prodcart q (prodcart alph q))). 2: apply dans_trans with d; 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 in |- *. intro. cut (exists y : Elt, dans y qa /\ couple e0 (couple epsilon e) = transition_back g0 y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht; intros y Ht; elim Ht; clear Ht; intros. unfold transition_back in H3. cut (e0 = y :>Elt /\ couple epsilon e = couple epsilon g0 :>Elt). 2: apply equal_couple; auto. intro Ht; elim Ht; clear Ht; intros. cut (epsilon = epsilon :>Elt /\ e = g0 :>Elt). 2: apply equal_couple; auto. intro Ht; elim Ht; clear Ht; intros. rewrite H4. auto. Qed.
imports: Ensf Max Words Dec Reg Rat