proposition: Lemma automate_A_D : forall (q qd qa d : Ensf) (g0 : Elt), automate q qd qa d -> automate_A (add g0 q) (singleton g0) qa (union d (delta_D g0 qd)).
proof: Proof. unfold automate_A in |- *. split. apply inclus_add. apply automate_def3 with qd d; auto. split; auto. apply union_inclus. apply inclus_trans with (prodcart q (prodcart alph q)). apply automate_def1 with qd qa; assumption. apply cart_inclus; auto. unfold delta_D in |- *. unfold inclus in |- *. intros x H2. cut (exists y : Elt, dans y qd /\ x = transition_D g0 y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht; intros t Ht; elim Ht; clear Ht; intros. rewrite H1. unfold transition_D in |- *. apply coupl2_inv; auto. apply coupl2_inv; auto. apply dans_add2. apply dans_trans with qd; auto. apply automate_def2 with qa d; auto. Qed.
imports: Ensf Max Words Dec