proposition: Lemma dstar_is_good : forall (q qa d : Ensf) (g0 : Elt), automate q (singleton g0) qa d -> inclus (fun_d_dstar g0 qa d) (prodcart q (prodcart (add epsilon alph) q)).
proof: Proof. intros. unfold fun_d_dstar in |- *. apply union_inclus. cut (inclus d (prodcart q (prodcart alph q))). 2: apply automate_def1 with (singleton g0) qa; assumption. intro. apply inclus_trans with (prodcart q (prodcart alph q)); auto. unfold delta in |- *. unfold inclus in |- *. intros. cut (exists y : Elt, dans y qa /\ x = transition_back g0 y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht; intros y Ht; elim Ht; clear Ht; intros H1 H2. rewrite H2. unfold transition_back in |- *. apply coupl2_inv. apply dans_trans with qa; auto. apply automate_def3 with (singleton g0) d; auto. apply coupl2_inv; auto. apply dans_trans with (singleton g0); auto. apply automate_def2 with qa d; auto. Qed.
imports: Ensf Max Words Dec Reg Rat