proposition: Lemma isregular_isregular_D_1 : forall (q qd qa d : Ensf) (g0 : Elt), automate q qd qa d -> ~ dans g0 q -> 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).
proof: Proof. intros. split. unfold eqwordset in |- *. intro w. split. unfold reconnait in |- *. intro Ht; elim Ht; clear Ht; intros H1 Ht; elim Ht; clear Ht; intros e1 Ht; elim Ht; clear Ht; intros e2 Ht; elim Ht; clear Ht; intros H2 Ht; elim Ht; clear Ht; intros. unfold reconnait_A in |- *. split. assumption. exists g0. exists e2. split; [ auto | split ]. assumption. apply chemin_A_epsilon with e1; auto. apply chemin_A_d1_d2 with d; auto. apply chemin_A_q1_q2 with q; auto. apply chemin_chemin_A; auto. apply union_d. unfold delta_D in |- *. replace (couple g0 (couple epsilon e1)) with (transition_D g0 e1); auto. unfold reconnait_A in |- *. intro Ht; elim Ht; clear Ht; intros H1 Ht; elim Ht; clear Ht; intros e1 Ht; elim Ht; clear Ht; intros e2 Ht; elim Ht; clear Ht; intros H2 Ht; elim Ht; clear Ht; intros. unfold reconnait in |- *. split. assumption. cut (e1 = g0 :>Elt); auto. intro. cut (exists e : Elt, dans e qd /\ chemin_A (add g0 q) (union d (delta_D g0 qd)) e e2 w). 2: apply chemin_A_g0_e2 with qa e1; auto. intro Ht; elim Ht; clear Ht; intros e Ht; elim Ht; clear Ht; intros. exists e. exists e2. split; [ assumption | split ]. assumption. apply chemin_D_chemin with qd qa g0; auto. apply dans_trans with qd; auto. apply automate_def2 with qa d; auto. intros. apply chemin_A_e1_g0 with q qd qa d g0 g0 g0; auto. Qed.
imports: Ensf Max Words Dec