proposition: Lemma Gunion_disj_Derivestar2 : ~ dans S X -> ~ dans S V1 -> ~ dans S V2 -> isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> inter V1 V2 empty -> forall u v : Word, Derivestar Ru u v -> inmonoid (union X V2) u -> Derivestar R2 u v.
proof: Proof. unfold Derivestar in |- *. intros N_dans_X N_dans_V1 N_dans_V2 G_1 G_2 inter_V1_V2_empty u v Derivestar_Ru. pattern u, v in |- *. apply Derivestar_Ru. auto. intros u0 v0 w Der_Ru inmon_v0_imp_Rstar_R2_v0 inmon_u0. apply Rstar_R with v0. prolog [ sym_inter isGram2 inter_union isGram4 inmon_Der_imp_Der_d2 ] 4. prolog [ inmon_Der_imp_inmon_d2 ] 3. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3