proposition: Lemma lword_is_reg : forall w : Word, inmonoid alph w -> isregular (lword w).
proof: Proof. unfold isregular in |- *. intros. 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 w))))). 2: apply lword_is_regS; auto. intro H0; elim H0; clear H0. 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 H0 H1. exists q. exists (singleton e). exists qa. exists d. auto. Qed.
imports: Ensf Max Words Dec Reg Rat