proposition: Lemma inmon_Der_imp_Der_d : ~ dans S X -> ~ dans S V1 -> ~ dans S V2 -> Regles X V1 R1 -> Regles X V2 R2 -> inter (union X V1) V2 empty -> forall u v : Word, Derive Ru u v -> inmonoid (union X V1) u -> Derive R1 u v.
proof: Proof. intros N_dans_X N_dans_V1 N_dans_V2 Re_1 Re_2 inter_X_V1_V2_empty u v Der_Ru_u. elim Der_Ru_u. intros u0 v0 A dans_couple_Ru inmon_cons_A_v0. apply Derive1. cut (couple S (word (cons S1 nil)) = couple A (word u0) :>Elt \/ dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))). intro temp; elim temp; clear temp. intro egal_S. absurd (dans S X \/ dans S V1). red in |- *. intro temp; elim temp; clear temp. exact N_dans_X. exact N_dans_V1. apply dans_union. replace S with A. prolog [ inmonoid_cons_inv2 ] 2. injection egal_S; auto. intro dans_couple_add. cut (couple S (word (cons S2 nil)) = couple A (word u0) :>Elt \/ dans (couple A (word u0)) (union R1 R2)). intro temp; elim temp; clear temp. intro egal_S. absurd (dans S X \/ dans S V1). red in |- *. intro temp; elim temp; auto. apply dans_union. replace S with A. prolog [ inmonoid_cons_inv2 ] 2. injection egal_S; auto. intro dans_couple_union. cut (dans (couple A (word u0)) R1 \/ dans (couple A (word u0)) R2). intro temp; elim temp; clear temp. auto. intro dans_R2. absurd (inter (union X V1) V2 empty). red in |- *. unfold inter in |- *. intro temp; elim temp; clear temp. intros HH temp; elim temp; clear temp; intros HHH HHHH. prolog [ Regles_inv1 inmonoid_cons_inv2 dans_empty_imp_P ] 4. assumption. auto. auto. auto. prolog [ inmonoid_cons_inv Derive2 ] 10. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3