proposition: Lemma automate_lconc_isgood : forall q1 qd1 qa1 d1 q2 qd2 qa2 d2 : Ensf, automate q1 qd1 qa1 d1 -> automate q2 qd2 qa2 d2 -> automate_A (union_disj q1 q2) (map injgauche qd1) (map injdroite qa2) (union (pont qa1 qd2) (union (injg_d1 q1 d1) (injd_d2 q2 d2))).
proof: Proof. intros. red in |- *. split. unfold union_disj in |- *. apply inclus_d2. apply map_inclus. apply automate_def3 with qd2 d2; auto. split. unfold union_disj in |- *. apply inclus_g2. apply map_inclus. apply automate_def2 with qa1 d1; auto. apply union_inclus. unfold pont in |- *. unfold inclus in |- *. intros. cut (exists y : Elt, dans y (prodcart qa1 qd2) /\ x = transition_pont y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht. intros y Ht; elim Ht; clear Ht; intros H2 H3. cut (exists y1 : Elt, (exists y2 : Elt, dans y1 qa1 /\ dans y2 qd2 /\ y = couple y1 y2 :>Elt)). 2: apply coupl3; auto. intro Ht; elim Ht; clear Ht. intros y1 Ht; elim Ht; clear Ht. intros y2 Ht; elim Ht; clear Ht. intros H4 Ht; elim Ht; clear Ht; intros H5 H6. cut (x = couple (couple y1 zero) (couple epsilon (couple y2 un)) :>Elt). 2: rewrite H3. 2: rewrite H6; auto. intro H7. rewrite H7. apply coupl2_inv. unfold union_disj in |- *. apply union_g. replace (couple y1 zero) with (injgauche y1); auto. apply dans_map_inv. apply dans_trans with qa1; auto. apply automate_def3 with qd1 d1; auto. apply coupl2_inv; auto. unfold union_disj in |- *. apply union_d. replace (couple y2 un) with (injdroite y2); auto. apply dans_map_inv. apply dans_trans with qd2; auto. apply automate_def2 with qa2 d2; auto. apply union_inclus. apply inclus_trans with (prodcart (map injgauche q1) (prodcart alph (map injgauche q1))). unfold injg_d1 in |- *. apply inclus_tq. unfold union_disj in |- *. apply cart_inclus. apply inclus_g. apply cart_inclus; auto. apply inclus_trans with (prodcart (map injdroite q2) (prodcart alph (map injdroite q2))). unfold injd_d2 in |- *. apply inclus_tq. unfold union_disj in |- *. apply cart_inclus; auto. Qed.
imports: Ensf Max Words Dec Reg Rat