proposition: Lemma Gunion_Derivestar : 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 V1) u -> Derivestar R1 u v.
proof: Proof. unfold Derivestar in |- *. intros 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_R1_v0 inmon_u0. apply Rstar_R with v0. prolog [ inmon_Der_imp_Der isGram4 inter_union isGram2 ] 5. prolog [ inmon_Der_imp_inmon ] 3. Qed.
imports: Ensf Words more_words need fonctions Relations gram