proposition: Lemma lword_is_regS : forall w : Word, inmonoid alph w -> exists q : Ensf, (exists e : Elt, (exists qa : Ensf, (exists d : Ensf, automate q (singleton e) qa d /\ eqwordset (reconnait q (singleton e) qa d) (lword w)))).
proof: Proof. simple induction w. intro. apply lwordnil_is_regS. intros a w0 H H4. cut (inmonoid alph w0). 2: apply (inmonoid_cons_inv alph w0 a); auto. intro H5. cut (exists q : Ensf, (exists e : Elt, (exists qa : Ensf, (exists d : Ensf, automate q (singleton e) qa d /\ eqwordset (reconnait q (singleton e) qa d) (lword w0))))); auto. clear H; intro H; elim H; clear H. intros q H0; elim H0; clear H0. intros e H0; elim H0; clear H0. intros qa H0; elim H0; clear H0. intros d H0; elim H0; clear H0. intros. cut (exists e0 : Elt, ~ dans e0 q). 2: apply exist_other; auto. intro H2; elim H2; clear H2. intros e0 H2. exists (add e0 q). exists e0. exists qa. exists (add (couple e0 (couple a e)) d). elim H; clear H. intros H H1. elim H1; clear H1. intros. split. red in |- *. split; auto. split; auto. apply add_inclus. apply coupl2_inv; auto. apply coupl2_inv. apply (inmonoid_cons_inv2 alph a w0); auto. cut (dans e q); auto. apply (inclus_trans d (prodcart q (prodcart alph q))); auto. apply auto_cons; auto. apply (inmonoid_cons_inv2 alph a w0); auto. unfold automate in |- *; auto. Qed.
imports: Ensf Max Words Dec Reg Rat