proposition: Lemma lunion_is_reg : forall l1 l2 : wordset, isregular l1 -> isregular l2 -> isregular (lunion l1 l2).
proof: Proof. unfold isregular in |- *. intros l1 l2 H1 H2. elim H1; clear H1. intros q1 H1; elim H1; clear H1; intros qd1 H1; elim H1; clear H1; intros qa1 H1; elim H1; clear H1; intros d1 H1; elim H1; clear H1. intros H1_aut H1_eq. elim H2; clear H2. intros q2 H2; elim H2; clear H2; intros qd2 H2; elim H2; clear H2; intros qa2 H2; elim H2; clear H2; intros d2 H2; elim H2; clear H2. intros H2_aut H2_eq. exists (union_disj q1 q2). exists (union_disj qd1 qd2). exists (union_disj qa1 qa2). exists (union (injg_d1 q1 d1) (injd_d2 q2 d2)). split. red in |- *. split. apply inclus_union_disj. apply automate_def3 with qd1 d1; auto. apply automate_def3 with qd2 d2; auto. split. apply inclus_union_disj. apply automate_def2 with qa1 d1; auto. apply automate_def2 with qa2 d2; auto. apply d_is_good. apply lunion_is_reg1; auto. Qed.
imports: Ensf Max Words Dec Reg Rat