proposition: Lemma inmon_Der_imp_Der2 : Regles X V1 R1 -> Regles X V2 R2 -> inter (union X V2) V1 empty -> forall u v : Word, Derive Ru u v -> inmonoid (union X V2) u -> Derive R2 u v.
proof: Proof. intros Re_1 Re_2 inter_X_V2_V1_empty u v Der_Ru_u. elim Der_Ru_u. intros u0 v0 A dans_couple_Ru inmon_cons_A_v0. apply Derive1. cut (dans (couple A (word u0)) R1 \/ dans (couple A (word u0)) R2). intro temp; elim temp; clear temp. intro dans_R1. absurd (inter (union X V2) V1 empty). red in |- *. unfold inter in |- *. intros (H1, (H2, H3)). apply dans_empty_imp_P with A. prolog [ inmonoid_cons_inv2 Regles_inv1 ] 3. assumption. trivial. auto. prolog [ Derive2 inmonoid_cons_inv ] 10. Qed.
imports: Ensf Words more_words need fonctions Relations gram