proposition: Lemma Gunion_disj_LG_inclus1 : ~ dans S X -> ~ dans S V1 -> ~ dans S V2 -> isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> inter V1 V2 empty -> l_inclus (LG X Vu Ru S) (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)).
proof: Proof. intros N_dans_X N_dans_V1 N_dans_V2 G_1 G_2 inter_V1_V2_empty. red in |- *. unfold LG in |- *. intros w temp; elim temp; clear temp; intros Der_Ru inmonoid_X_w. unfold lunion in |- *. elimtype (cons S nil = w :>Word \/ Derivestar R1 (cons S1 nil) w \/ Derivestar R2 (cons S2 nil) w). intro eg_cons_S_nil_w. absurd (dans S X). assumption. apply inmonoid_cons_inv2 with nil. rewrite eg_cons_S_nil_w; assumption. intro temp; elim temp; clear temp; auto. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3