proposition: Lemma isregular_isregular_D : forall l : wordset, isregular l -> isregular_D l.
proof: Proof. intro l. unfold isregular at 1 in |- *. intro Ht; elim Ht; clear Ht; intros q Ht; elim Ht; clear Ht; intros qd Ht; elim Ht; clear Ht; intros qa Ht; elim Ht; clear Ht; intros d Ht; elim Ht; clear Ht; intros. cut (exists g0 : Elt, ~ dans g0 q). 2: apply exist_other. intro Ht; elim Ht; clear Ht; intros g0 H1. cut (automate_A (add g0 q) (singleton g0) qa (union d (delta_D g0 qd))). 2: apply automate_A_D; auto. intro. unfold isregular_D in |- *. exists (add g0 q). exists g0. exists (sync_qa (add g0 q) qa (union d (delta_D g0 qd))). exists (sync_d (add g0 q) (union d (delta_D g0 qd))). split. apply automateA_automate; auto. cut (eqwordset (reconnait q qd qa d) (reconnait_A (add g0 q) (singleton g0) qa (union d (delta_D g0 qd))) /\ (forall w : Word, chemin_A (add g0 q) (union d (delta_D g0 qd)) g0 g0 w -> w = nil :>Word)). 2: apply isregular_isregular_D_1; auto. intro Ht; elim Ht; clear Ht; intros. split. intros w H5. cut (chemin_A (add g0 q) (union d (delta_D g0 qd)) g0 g0 w). 2: apply chemin_cheminA with (singleton g0) qa; auto. intro. apply (H4 w); auto. apply eqwordset_trans with (reconnait_A (add g0 q) (singleton g0) qa (union d (delta_D g0 qd))). unfold eqwordset in |- *. intro w. split. intro. apply reconnait_reconnaitA; auto. intro. apply reconnaitA_reconnait; auto. apply eqwordset_trans with (reconnait q qd qa d); auto. apply eqwordset_sym; assumption. Qed.
imports: Ensf Max Words Dec