proposition: Lemma chemin_g0_g0 : forall (q qa d : Ensf) (g0 : Elt) (w0 : Word), automate q (singleton g0) qa d -> (forall e x : Elt, dans (couple g0 (couple x e)) d -> x = epsilon :>Elt) -> chemin g0 g0 q d w0 -> w0 = nil :>Word.
proof: Proof. intros q qa d g0 w0 H_aut H_g0. generalize w0; clear w0; simple induction w0. auto. intros x w H H0. cut (Chemin g0 g0 q d (cons x w)); auto. intro. cut (exists e : Elt, chemin e g0 q d w /\ dans g0 q /\ dans x alph /\ dans (couple g0 (couple x e)) d); auto. intro Ht; elim Ht; clear Ht; intros e Ht; elim Ht; clear Ht; intros H2 Ht; elim Ht; clear Ht; intros H3 Ht; elim Ht; clear Ht; intros H4 H5. cut (x = epsilon :>Elt). 2: apply (H_g0 e x); assumption. intro. absurd (dans x alph); auto. rewrite H6. red in |- *; intro; apply not_dans_epsilon_alph; assumption. Qed.
imports: Ensf Max Words Dec Reg Rat