proposition: Lemma lstar_is_reg1 : forall (q qa d : Ensf) (l : wordset) (g0 : Elt) (w : Word), automate q (singleton g0) qa d -> (forall w : Word, chemin g0 g0 q d w -> w = nil :>Word) -> eqwordset (reconnait q (singleton g0) qa d) l -> reconnait_A q (singleton g0) (singleton g0) (fun_d_dstar g0 qa d) w -> lstar l w.
proof: Proof. intros. elim H2; clear H2; intros H2 Ht; elim Ht; clear Ht; intros e1 Ht; elim Ht; clear Ht; intros e2 Ht; elim Ht; clear Ht; intros H3 Ht; elim Ht; clear Ht; intros H4 H5. cut (chemin e1 e2 q d w \/ (exists e : Elt, (exists w1 : Word, (exists w2 : Word, chemin e1 e q d w1 /\ dans e qa /\ lstar l w2 /\ w = Append w1 w2 :>Word)))). 2: apply lstar_is_reg2_bis with g0; auto. intro Ht; elim Ht; clear Ht. intro. cut (e1 = g0 :>Elt); auto. cut (e2 = g0 :>Elt); auto. intros. cut (chemin g0 g0 q d w). 2: cut (chemin e1 e2 q d w); auto. 2: rewrite H7; rewrite H8; auto. intro. cut (w = nil :>Word). 2: apply (H0 w); assumption. intro H10. rewrite H10. unfold lstar in |- *. exists 0. unfold lpuiss in |- *. unfold lword in |- *; auto. intro Ht; elim Ht; clear Ht; intros e Ht; elim Ht; clear Ht; intros w1 Ht; elim Ht; clear Ht; intros w2 Ht; elim Ht; clear Ht; intros H6 Ht; elim Ht; clear Ht; intros H7 Ht; elim Ht; clear Ht; intros H8 H9. elim H8. intros n H10. unfold lstar in |- *. exists (S n). change (lconc l (lpuiss n l) w) in |- *. unfold lconc in |- *. exists w1. exists w2. split. 2: split; [ assumption | assumption ]. unfold eqwordset in H1. elim (H1 w1); intros. apply H11. unfold reconnait in |- *. split. apply (Cheminmonoid w1 q (singleton g0) qa d H e1 e H6); auto. exists e1. exists e. auto. Qed.
imports: Ensf Max Words Dec Reg Rat