proposition: Lemma Gunion_disj_Derive1 : ~ dans S X -> ~ dans S V1 -> ~ dans S V2 -> isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> forall u : Word, Derive Ru (cons S nil) u -> cons S1 nil = u :>Word \/ cons S2 nil = u :>Word.
proof: Proof. intros N_dans_X N_dans_V1 N_dans_V2 G_1 G_2 u Derive_Ru. cut (Derive_inv Ru (cons S nil) u). unfold Derive_inv in |- *. simpl in |- *. intro temp; elim temp; clear temp; intro temp; elim temp; clear temp. intros x dans_S_x_Ru temp. elim temp; clear temp. intros x0 egal_S_x0_S_nil egal_Append_x_x0_u. replace u with x. cut (couple S (word (cons S1 nil)) = couple S (word x) :>Elt \/ dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))). intro temp; elim temp; clear temp. intro egal_S. injection egal_S; auto. intro dans_couple_add. cut (couple S (word (cons S2 nil)) = couple S (word x) :>Elt \/ dans (couple S (word x)) (union R1 R2)). intro temp; elim temp; clear temp. intro egal_S. injection egal_S; auto. intro dans_couple_union. cut (dans (couple S (word x)) R1 \/ dans (couple S (word x)) R2). intro temp; elim temp; clear temp. intro dans_R1. absurd (dans S V1). assumption. prolog [ isGram4 Regles_inv1 ] 3. intros dans_R2. absurd (dans S V2). assumption. prolog [ isGram4 Regles_inv1 ] 3. auto. auto. auto. replace x with (Append x nil). replace nil with x0. assumption. apply cons_cons_inv2 with S S; assumption. apply Append_w_nil. intros. cut (Derive_inv Ru nil x). unfold Derive_inv in |- *. simpl in |- *. tauto. auto. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3