proposition: Lemma lstar_is_reg : forall l : wordset, isregular l -> isregular (lstar l).
proof: Proof. intros l H. cut (isregular_D l). 2: apply isregular_isregular_D; auto. clear H; intro H; elim H; clear H. intros q H; elim H; clear H; intros g0 H; elim H; clear H; intros qa H; elim H; clear H; intros d H; elim H; clear H. intros H_aut Ht; elim Ht; clear Ht; intros H_g0 H_eq. apply isregular_A_isregular. unfold isregular_A in |- *. exists q. exists (singleton g0). exists (singleton g0). exists (fun_d_dstar g0 qa d). split. red in |- *. elim H_aut. intros H0 H1; elim H1; clear H1; intros H1 H2. split; [ assumption | split ]. assumption. apply dstar_is_good; assumption. unfold eqwordset in |- *. intro w. split. intro; apply lstar_is_reg1 with q qa d g0; auto. intro; pattern w in |- *; apply induction_star with l; auto. simple induction n. unfold lpuiss in |- *. unfold lword in |- *. intros. rewrite <- H0. unfold reconnait_A in |- *. split; auto. exists g0. exists g0. split; [ auto | split ]. auto. apply chemin_A_nil; auto. apply dans_trans with (singleton g0); auto. apply automate_def2 with qa d; auto. intros y H1 w0. change (lconc l (lpuiss y l) w0 -> reconnait_A q (singleton g0) (singleton g0) (fun_d_dstar g0 qa d) w0) in |- *. unfold lconc in |- *. intros Ht; elim Ht; clear Ht; intros w1 Ht; elim Ht; clear Ht; intros w2 Ht; elim Ht; clear Ht; intros H2 Ht; elim Ht; clear Ht; intros H3 H4. cut (reconnait_A q (singleton g0) (singleton g0) (fun_d_dstar g0 qa d) w2); auto. intro H5. unfold eqwordset in H_eq. elim (H_eq w1); intros H6 H7. cut (reconnait q (singleton g0) qa d w1); auto. intro H8. clear H6 H7 H1 H_eq. elim H8; clear H8; intros H8 Ht; elim Ht; clear Ht; intros e1 Ht; elim Ht; clear Ht; intros e2 Ht; elim Ht; clear Ht; intros H9 Ht; elim Ht; clear Ht; intros H10 H11. elim H5; clear H5; intros H12 Ht; elim Ht; clear Ht; intros e3 Ht; elim Ht; clear Ht; intros e4 Ht; elim Ht; clear Ht; intros H13 Ht; elim Ht; clear Ht; intros H14 H15. unfold reconnait_A in |- *. split. rewrite H4. apply inmonoid_Append; auto. exists e1. exists e4. split; [ assumption | split ]. assumption. rewrite H4. apply chemin_Append with e2. apply chemin_A_d1_d2 with d. apply chemin_chemin_A; auto. unfold fun_d_dstar in |- *. apply inclus_g. apply chemin_A_epsilon with e3; auto. apply dans_trans with qa; auto. apply automate_def3 with (singleton g0) d; auto. unfold fun_d_dstar in |- *. apply union_d. unfold delta in |- *. cut (e3 = g0 :>Elt); auto. intro H16. rewrite H16. replace (couple e2 (couple epsilon g0)) with (transition_back g0 e2); auto. Qed.
imports: Ensf Max Words Dec Reg Rat