proposition: Lemma lstar_is_reg2_bis : forall (q qa d : Ensf) (g0 e1 e2 : Elt) (w : Word) (l : wordset), automate q (singleton g0) qa d -> eqwordset (reconnait q (singleton g0) qa d) l -> (forall w : Word, chemin g0 g0 q d w -> w = nil :>Word) -> chemin_A q (fun_d_dstar g0 qa d) e1 e2 w -> e2 = g0 :>Elt -> 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))).
proof: Proof. intros q qa d g0 e1 e2 w l H H_eq H_g0 H0. elim H0. intros. left. apply chemin_nil; auto. intros e0 e e3 x w0 H1 H2 H3 H4 H5 H6. cut (dans (couple e0 (couple x e)) d). 2: apply transition_dans_l with q qa g0; auto. intro. elim H2; clear H2. 3: assumption. intro. left. apply chemin_cons with e; auto. intro Ht; elim Ht; clear Ht; intros x1 Ht; elim Ht; clear Ht; intros w1 Ht; elim Ht; clear Ht; intros w2 Ht; elim Ht; clear Ht; intros H8 Ht; elim Ht; clear Ht; intros H9 Ht; elim Ht; clear Ht; intros H10 H11. right. exists x1. exists (cons x w1). exists w2. split. apply chemin_cons with e; auto. split; [ assumption | split ]. assumption. replace (Append (cons x w1) w2) with (cons x (Append w1 w2)); auto. intros e0 e e3 w0 H1 H2 H3 H4 H5. right. cut (dans e0 qa /\ e = g0 :>Elt). 2: apply transition_par_epsilon with q d; auto. intro Ht; elim Ht; clear Ht; intros. elim H2; clear H2. 3: assumption. rewrite H7. rewrite H5. intro. cut (w0 = nil :>Word). 2: apply (H_g0 w0); assumption. intro. exists e0. exists nil. exists nil. split. apply chemin_nil; auto. split; [ assumption | split ]. unfold lstar in |- *. exists 0. unfold lpuiss in |- *. unfold lword in |- *; auto. rewrite H8; auto. intro Ht; elim Ht; clear Ht; intros x1 Ht; elim Ht; clear Ht; intros w1 Ht; elim Ht; clear Ht; intros w2 Ht; elim Ht; clear Ht; intros H8 Ht; elim Ht; clear Ht; intros H9 Ht; elim Ht; clear Ht; intros H10 H11. exists e0. exists nil. exists (Append w1 w2). split. apply chemin_nil; auto. split; [ assumption | split ]. 2: replace (Append nil (Append w1 w2)) with (Append w1 w2); auto. elim H10. intros n H12. unfold lstar in |- *. exists (S n). change (lconc l (lpuiss n l) (Append w1 w2)) in |- *. unfold lconc in |- *. exists w1. exists w2. split. 2: split; [ assumption | auto ]. unfold eqwordset in H_eq. elim (H_eq w1); intros. apply H2. unfold reconnait in |- *. split. apply (Cheminmonoid w1 q (singleton g0) qa d H e x1 H8); auto. exists e. exists x1. split; [ rewrite H7; auto | split; [ assumption | assumption ] ]. Qed.
imports: Ensf Max Words Dec Reg Rat