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