proposition: Lemma lconc_is_reg : forall l1 l2 : wordset, isregular l1 -> isregular l2 -> isregular (lconc l1 l2).
proof: Proof. intros. unfold isregular in H. elim H; clear H. intros q1 H; elim H; clear H; intros qd1 H; elim H; clear H; intros qa1 H; elim H; clear H; intros d1 H; elim H; clear H. intros H_aut H_eq. unfold isregular in H0. elim H0; clear H0. intros q2 H0; elim H0; clear H0; intros qd2 H0; elim H0; clear H0; intros qa2 H0; elim H0; clear H0; intros d2 H0; elim H0; clear H0. intros H0_aut H0_eq. apply isregular_A_isregular. unfold isregular_A in |- *. exists (union_disj q1 q2). exists (map injgauche qd1). exists (map injdroite qa2). exists (union (pont qa1 qd2) (union (injg_d1 q1 d1) (injd_d2 q2 d2))). split. apply automate_lconc_isgood; auto. apply lconc_is_reg1; auto. Qed.
imports: Ensf Max Words Dec Reg Rat