(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 gram4.v                                  *)
(****************************************************************************)
(*              Formal Language Theory                                      *)
(*                                                                          *)
(*              Judicael Courant - Jean-Christophe Filliatre                *)
(*                                                                          *)
(*              Developped in V5.8  June-July 1993                          *)
(*              Ported     to V5.10 October 1994                            *)
(****************************************************************************)

Require Import Ensf.
Require Import Words.
Require Import more_words.
Require Import Rat.
Require Import need.
Require Import fonctions.
Require Import Relations.
Require Import gram.
Require Import gram2.
Require Import gram3.

Section gram4.

Variable X V1 R1 : Ensf.
Variable S1 : Elt.

Variable V2 R2 : Ensf.
Variable S2 : Elt.

Variable S : Elt.
Let C := Gunion_disj_p V1 R1 S1 V2 R2 S2 S.
Let Vu := fst C.
Let C' := snd C.
Let Ru := fst C'.
Let Su := snd C'.

Lemma inter_X_V1_u_V2 :
 isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> inter X (union V1 V2) empty.

(* Goal: forall (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2), inter X (union V1 V2) empty *)
prolog [ isGram2 union_inter ] 5.
(*Intro G1.
Intro G2.
Apply union_inter.
Apply isGram2 with R1 S1; Assumption.
Apply isGram2 with R2 S2; Assumption.*)
Qed.

Lemma inter_X_Vu_d :
 isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> ~ dans S X -> inter X Vu empty.
(* Goal: forall (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : not (dans S X)), inter X Vu empty *)
intros G_1 G_2 N_dans_S_X.
(* Goal: forall _ : inter (union X V2) V1 empty, False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
unfold inter in |- *.
(* Goal: and (Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) w) (inmonoid X w) *)
split.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
 auto.
(* Goal: and (Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) w) (inmonoid X w) *)
 split.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
  auto.
(* Goal: forall (x : Elt) (_ : dans x X) (_ : dans x Vu), dans x empty *)
  intros x dans_x_X dans_x_Vu.
(* Goal: dans x empty *)
  absurd (dans x X).
(* Goal: not (dans x X) *)
(* Goal: dans x X *)
  cut (S = x :>Elt \/ dans x (union V1 V2)). (**)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
  intro temp; elim temp; clear temp.
(* Goal: forall _ : @eq Elt S x, not (dans x X) *)
(* Goal: forall _ : dans x (union V1 V2), not (dans x X) *)
(* Goal: or (@eq Elt S x) (dans x (union V1 V2)) *)
(* Goal: dans x X *)
	intros egal_S_x.
(* Goal: not (dans x X) *)
(* Goal: forall _ : dans x (union V1 V2), not (dans x X) *)
(* Goal: or (@eq Elt S x) (dans x (union V1 V2)) *)
(* Goal: dans x X *)
	rewrite <- egal_S_x; assumption.

(* Goal: forall _ : dans x (union V1 V2), not (dans x X) *)
(* Goal: or (@eq Elt S x) (dans x (union V1 V2)) *)
(* Goal: dans x X *)
	intro dans_x_V1_u_V2.
(* Goal: not (dans x X) *)
(* Goal: or (@eq Elt S x) (dans x (union V1 V2)) *)
(* Goal: dans x X *)
	prolog [ inter_X_V1_u_V2 sym_inter inter_dans ] 4.
	(*Apply inter_dans with (union V1 V2).
		Apply sym_inter.
		Apply inter_X_V1_u_V2;Assumption.

		Assumption.*)

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
  (**)auto.

(* Goal: inmonoid X w *)
  assumption.
Qed.

Lemma Gunion_disj_Regles :
 isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> Regles X Vu Ru.
(* Goal: forall (_ : not (dans S X)) (_ : not (dans S V1)) (_ : not (dans S V2)) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty), l_egal (LG X Vu Ru S) (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) *)
intros.
(* Goal: Regles X Vu Ru *)
unfold Vu, Ru in |- *; simpl in |- *.
(* Goal: Regles X (add S (union V1 V2)) (add (couple S (word (cons S2 nil))) (union R1 R2)) *)
(* Goal: dans S (add S (union V1 V2)) *)
(* Goal: inmonoid (union X (add S (union V1 V2))) (cons S1 nil) *)
apply Regles_add.
(* Goal: Regles X (add S (union V1 V2)) (add (couple S (word (cons S2 nil))) (union R1 R2)) *)
(* Goal: dans S (add S (union V1 V2)) *)
(* Goal: inmonoid (union X (add S (union V1 V2))) (cons S1 nil) *)
apply Regles_add.
(* Goal: Regles X (add S (union V1 V2)) (union R1 R2) *)
(* Goal: dans S (add S (union V1 V2)) *)
(* Goal: inmonoid (union X (add S (union V1 V2))) (cons S2 nil) *)
(* Goal: dans S (add S (union V1 V2)) *)
(* Goal: inmonoid (union X (add S (union V1 V2))) (cons S1 nil) *)
apply Regles_add2.
change (Regles X (fst (Gunion V1 R1 V2 R2)) (snd (Gunion V1 R1 V2 R2)))
 in |- *.
(* Goal: Regles X (@fst Ensf Ensf (Gunion V1 R1 V2 R2)) (@snd Ensf Ensf (Gunion V1 R1 V2 R2)) *)
(* Goal: dans S (add S (union V1 V2)) *)
(* Goal: inmonoid (union X (add S (union V1 V2))) (cons S2 nil) *)
(* Goal: dans S (add S (union V1 V2)) *)
(* Goal: inmonoid (union X (add S (union V1 V2))) (cons S1 nil) *)
prolog [ Gunion_Regles ] 2.
(*Apply Gunion_Regles with S1 S2;Auto.*)
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
auto.
(* Goal: inmonoid (union X (add S (union V1 V2))) (cons S1 nil) *)
apply inmonoid_cons.
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
trivial.
cut (dans S2 V2);
 [ auto
 | prolog [ isGram3 ] 2(*Apply isGram3 with X R2;Assumption*) ].

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
auto.

(* Goal: inmonoid (union X (add S (union V1 V2))) (cons S1 nil) *)
apply inmonoid_cons.
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
trivial.
cut (dans S1 V1);
 [ auto
 | prolog [ isGram3 ] 2 (*Apply isGram3 with X R1;Assumption*) ].

Qed.

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.
intros N_dans_X N_dans_V1 N_dans_V2 Re_1 Re_2 inter_X_V1_V2_empty u v
 Der_Ru_u.
(* Goal: forall _ : inmonoid (union X V2) u, Derive R2 u v *)
elim Der_Ru_u.
(* Goal: forall (u v : Word) (A : Elt) (_ : dans (couple A (word u)) Ru) (_ : inmonoid (union X V2) (cons A v)), Derive R2 (cons A v) (Append u v) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	intros u0 v0 A dans_couple_Ru inmon_cons_A_v0.
(* Goal: Derive R2 (cons A v0) (Append u0 v0) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	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))). (**)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : @eq Elt (couple S (word (cons S2 nil))) (couple S (word x)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro egal_S.
(* Goal: dans (couple A (word u0)) R1 *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R1 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
	absurd (dans S X \/ dans S V1).
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
	red in |- *.
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : dans S X, False *)
(* Goal: forall _ : dans S V1, False *)
(* Goal: or (dans S X) (dans S V1) *)
(* Goal: forall _ : dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2)), dans (couple A (word u0)) R1 *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
	exact N_dans_X.
(* Goal: forall _ : dans S V1, False *)
(* Goal: or (dans S X) (dans S V1) *)
(* Goal: forall _ : dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2)), dans (couple A (word u0)) R1 *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
	exact N_dans_V1.
(* Goal: or (dans S X) (dans S V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	apply dans_union.
(* Goal: dans S (union X V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	replace S with A.
(* Goal: dans A (union X V2) *)
(* Goal: @eq Elt A S *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	prolog [ inmonoid_cons_inv2 ] 2.
	(*Apply inmonoid_cons_inv2 with v0;Assumption.*)
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	injection egal_S; auto.

(* Goal: forall _ : dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro dans_couple_add.
	cut
  (couple S (word (cons S2 nil)) = couple A (word u0) :>Elt \/
   dans (couple A (word u0)) (union R1 R2)). (***)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : @eq Elt (couple S (word (cons S2 nil))) (couple S (word x)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro egal_S.
(* Goal: dans (couple A (word u0)) R1 *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R1 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
	absurd (dans S X \/ dans S V1).
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
	red in |- *.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	intro temp; elim temp; auto.

(* Goal: or (dans S X) (dans S V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	apply dans_union.
(* Goal: dans S (union X V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	replace S with A.
(* Goal: dans A (union X V2) *)
(* Goal: @eq Elt A S *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	prolog [ inmonoid_cons_inv2 ] 2.
	(*Apply inmonoid_cons_inv2 with v0;Assumption.*)
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	injection egal_S; auto.

(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro dans_couple_union.	
(* Goal: dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	cut (dans (couple A (word u0)) R1 \/ dans (couple A (word u0)) R2). (****)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	(*Intuition.*)intro temp; elim temp; clear temp.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
		auto.
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R1 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
		intro dans_R2.
(* Goal: dans (couple A (word u0)) R1 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
		absurd (inter (union X V1) V2 empty).
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
			red in |- *.
(* Goal: forall _ : inter (union X V2) V1 empty, False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			unfold inter in |- *.
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
			(*Intuition.*)intro temp; elim temp; clear temp.
(* Goal: forall (_ : inclus empty (union X V1)) (_ : and (inclus empty V2) (forall (x : Elt) (_ : dans x (union X V1)) (_ : dans x V2), dans x empty)), False *)
(* Goal: inter (union X V1) V2 empty *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
				      intros HH temp; elim temp; clear temp; intros HHH HHHH.
			(*Intros.*)
(* Goal: False *)
(* Goal: inter (union X V1) V2 empty *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
			prolog [ Regles_inv1 inmonoid_cons_inv2 dans_empty_imp_P ] 4.
			(*Intro temp;Elim temp;Clear temp.
			Intros incl_empty_X_V1 temp;Elim temp;Clear temp.
			Intros incl_empty_V2 imp.

			Apply dans_empty_imp_P with A.
			Apply imp.
				Apply inmonoid_cons_inv2 with v0;Assumption.
				Apply Regles_inv1 with X R2 (word u0);
						Assumption.*)
(* Goal: inmonoid X w *)
		assumption.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(****)auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(***)auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(**)auto.

(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	prolog [ inmonoid_cons_inv Derive2 ] 10.
	(*Intros u0 v0 x Der_Ru imp inmon_cons_x_u0.
	Apply Derive2.
	Apply imp.
	Apply inmonoid_cons_inv with x.
	Assumption.*)
Qed.

Lemma inmon_Der_imp_inmon_R1_d :
 forall u v : Word,
 Regles X V1 R1 ->
 Derive R1 u v -> inmonoid (union X V1) u -> inmonoid (union X V1) v.
(* Goal: forall (u v : Word) (_ : Regles X V1 R1) (_ : Derive R1 u v) (_ : inmonoid (union X V1) u), inmonoid (union X V1) v *)
prolog [ in_mon_X_Der_imp_inmon_X ] 7.
(*Intros.
Apply in_mon_X_Der_imp_inmon_X with R1 u;Assumption.*)
Qed.

Lemma inmon_Der_imp_inmon_d :
 ~ dans S X ->
 ~ dans S V1 ->
 ~ dans S V2 ->
 forall u v : Word,
 isGram X V1 R1 S1 ->
 isGram X V2 R2 S2 ->
 inter V1 V2 empty ->
 inmonoid (union X V1) u -> Derive Ru u v -> inmonoid (union X V1) v.
prolog
 [ isGram2 isGram4 inter_union inmon_Der_imp_Der_d inmon_Der_imp_inmon_R1_d ]
 15.
(*Intros N_dans_X N_dans_V1 N_dans_V2 u v G_R1 G_R2 inter_V1_V2_empty inmon_X_V1_u Der_Ru_u_v.
Apply inmon_Der_imp_inmon_R1_d with u.
	Apply isGram4 with S1;Assumption.

		Apply inmon_Der_imp_Der_d.

		Assumption.

		Assumption.

		Assumption.

		Apply isGram4 with S1;Assumption.

		Apply isGram4 with S2;Assumption.

		Apply inter_union.
			Apply isGram2 with R2 S2; Assumption.
			Assumption.

		Assumption.

		Assumption.

	Assumption.*)
Qed.

Lemma Gunion_disj_Derivestar :
 ~ 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 V1) u -> Derivestar R1 u v.
(* Goal: forall (_ : not (dans S X)) (_ : not (dans S V1)) (_ : not (dans S V2)) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty) (u v : Word) (_ : Derivestar Ru u v) (_ : inmonoid (union X V2) u), Derivestar R2 u v *)
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.
(* Goal: forall _ : inmonoid (union X V2) u, Rstar Word (Derive R2) u v *)
pattern u, v in |- *.
(* Goal: (fun w w0 : Word => forall _ : inmonoid (union X V2) w, Rstar Word (Derive R2) w w0) u v *)
apply Derivestar_Ru.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	auto.

(* Goal: forall (u v w : Word) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) v, Rstar Word (Derive R1) v w) (_ : inmonoid (union X V1) u), Rstar Word (Derive R1) u w *)
	intros u0 v0 w Der_Ru inmon_v0_imp_Rstar_R1_v0 inmon_u0. 
	apply Rstar_R with v0;
  prolog
   [ isGram2 inter_union isGram4 inmon_Der_imp_Der_d inmon_Der_imp_inmon_d ]
   4.
	(*Apply Rstar_R with v0
		inmon_v0_imp_Rstar_R1_v0 inmon_Der_imp_inmon_d.
		Apply inmon_Der_imp_Der_d.
			Assumption.
			Assumption.
			Assumption.
			Apply isGram4 with S1;Assumption.
			Apply isGram4 with S2;Assumption.
			Apply inter_union.
				Apply isGram2 with R2 S2; Assumption.
				Assumption.
			Assumption.
			Assumption.

		Apply inmon_v0_imp_Rstar_R1_v0.
		Apply inmon_Der_imp_inmon_d with u0;Assumption.*)
Qed.

Lemma inmon_Der_imp_Der_d2 :
 ~ dans S X ->
 ~ dans S V1 ->
 ~ dans S V2 ->
 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.
intros N_dans_X N_dans_V1 N_dans_V2 Re_1 Re_2 inter_X_V2_V1_empty u v
 Der_Ru_u.
(* Goal: forall _ : inmonoid (union X V2) u, Derive R2 u v *)
elim Der_Ru_u.
(* Goal: forall (u v : Word) (A : Elt) (_ : dans (couple A (word u)) Ru) (_ : inmonoid (union X V2) (cons A v)), Derive R2 (cons A v) (Append u v) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	intros u0 v0 A dans_couple_Ru inmon_cons_A_v0.
(* Goal: Derive R2 (cons A v0) (Append u0 v0) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	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))). (**)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : @eq Elt (couple S (word (cons S2 nil))) (couple S (word x)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro egal_S.
(* Goal: dans (couple A (word u0)) R2 *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	absurd (dans S X \/ dans S V2).
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
	red in |- *.
(* Goal: forall _ : or (dans S X) (dans S V2), False *)
(* Goal: or (dans S X) (dans S V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	intuition.
(* Goal: or (dans S X) (dans S V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	apply dans_union.
(* Goal: dans S (union X V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	replace S with A.
(* Goal: dans A (union X V2) *)
(* Goal: @eq Elt A S *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	prolog [ inmonoid_cons_inv2 ] 2.
	(*Apply inmonoid_cons_inv2 with v0;Assumption.*)
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	injection egal_S; auto.

(* Goal: forall _ : dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro dans_couple_add.
	cut
  (couple S (word (cons S2 nil)) = couple A (word u0) :>Elt \/
   dans (couple A (word u0)) (union R1 R2)). (***)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : @eq Elt (couple S (word (cons S2 nil))) (couple S (word x)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro egal_S.
(* Goal: dans (couple A (word u0)) R2 *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	absurd (dans S X \/ dans S V2).
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
	red in |- *.
(* Goal: forall _ : or (dans S X) (dans S V2), False *)
(* Goal: or (dans S X) (dans S V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	intuition.
(* Goal: or (dans S X) (dans S V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	apply dans_union.
(* Goal: dans S (union X V2) *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	replace S with A.
(* Goal: dans A (union X V2) *)
(* Goal: @eq Elt A S *)
(* Goal: forall _ : dans (couple A (word u0)) (union R1 R2), dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	prolog [ inmonoid_cons_inv2 ] 2.
	(*Apply inmonoid_cons_inv2 with v0;Assumption.*)
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	injection egal_S; auto.

(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro dans_couple_union.	
(* Goal: dans (couple A (word u0)) R2 *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	cut (dans (couple A (word u0)) R1 \/ dans (couple A (word u0)) R2). (****)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	(*Intuition.*) intro temp; elim temp; clear temp.
(* Goal: forall _ : dans (couple S (word x)) R1, or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) R2, or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (dans (couple S (word x)) R1) (dans (couple S (word x)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
		intro dans_R1.
(* Goal: dans (couple A (word u0)) R2 *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
		absurd (inter (union X V2) V1 empty).
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
			red in |- *.
(* Goal: forall _ : inter (union X V2) V1 empty, False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			unfold inter in |- *.
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
			(*Intuition.*) intro temp; elim temp; clear temp.
(* Goal: forall (_ : inclus empty (union X V2)) (_ : and (inclus empty V1) (forall (x : Elt) (_ : dans x (union X V2)) (_ : dans x V1), dans x empty)), False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
				 intros inc_empt temp; elim temp; clear temp.
(* Goal: forall (_ : inclus empty V1) (_ : forall (x : Elt) (_ : dans x (union X V2)) (_ : dans x V1), dans x empty), False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			intros incl_empty_V1 imp_dans_empty.
(* Goal: False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			apply dans_empty_imp_P with A.
(* Goal: dans A empty *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			apply imp_dans_empty; prolog [ Regles_inv1 inmonoid_cons_inv2 ] 4.
			(*Intro temp;Elim temp;Clear temp.
			Intros incl_empty_X_V2 temp;Elim temp;Clear temp.
			Intros incl_empty_V1 imp.
			Apply dans_empty_imp_P with A.
			Apply imp.
				Apply inmonoid_cons_inv2 with v0;Assumption.
				Apply Regles_inv1 with X R1 (word u0);
						Assumption.*)

(* Goal: inmonoid X w *)
		assumption.


(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple A (word u0))) (dans (couple A (word u0)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple A (word u0))) (dans (couple A (word u0)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
		trivial.
		
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(****)auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(***)auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(**)auto.

(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	prolog [ inmonoid_cons_inv Derive2 ] 10.
	(*Intros u0 v0 x Der_Ru imp inmon_cons_x_u0.
	Apply Derive2.
	Apply imp.
	Apply inmonoid_cons_inv with x.
	Assumption.*)
Qed.

Lemma inmon_Der_imp_inmon_R2_d :
 forall u v : Word,
 Regles X V2 R2 ->
 Derive R2 u v -> inmonoid (union X V2) u -> inmonoid (union X V2) v.
(* Goal: forall (u v : Word) (_ : Regles X V2 R2) (_ : Derive R2 u v) (_ : inmonoid (union X V2) u), inmonoid (union X V2) v *)
prolog [ in_mon_X_Der_imp_inmon_X ] 10.
(*Intros.
Apply in_mon_X_Der_imp_inmon_X with R2 u;Assumption.*)
Qed.


Lemma inmon_Der_imp_inmon_d2 :
 ~ dans S X ->
 ~ dans S V1 ->
 ~ dans S V2 ->
 forall u v : Word,
 isGram X V1 R1 S1 ->
 isGram X V2 R2 S2 ->
 inter V1 V2 empty ->
 inmonoid (union X V2) u -> Derive Ru u v -> inmonoid (union X V2) v.
prolog
 [ sym_inter isGram2 inter_union isGram4 inmon_Der_imp_Der_d2
  inmon_Der_imp_inmon_R2_d ] 15.
(*Intros N_dans_X N_dans_V1 N_dans_V2 u v G_R1 G_R2 inter_V1_V2_empty inmon_X_V2_u Der_Ru_u_v.
Apply inmon_Der_imp_inmon_R2_d with u.
 	Apply isGram4 with S2;Assumption.

	Apply inmon_Der_imp_Der_d2.

		Assumption.

		Assumption.

		Assumption.

		Apply isGram4 with S1;Assumption.

		Apply isGram4 with S2;Assumption.

		Apply inter_union.
			Apply isGram2 with R1 S1; Assumption.
			Apply sym_inter;Assumption.

		Assumption.

		Assumption.

	Assumption.*)
Qed.

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.
(* Goal: forall (_ : not (dans S X)) (_ : not (dans S V1)) (_ : not (dans S V2)) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty) (u v : Word) (_ : Derivestar Ru u v) (_ : inmonoid (union X V2) u), Derivestar R2 u v *)
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.
(* Goal: forall _ : inmonoid (union X V2) u, Rstar Word (Derive R2) u v *)
pattern u, v in |- *.
(* Goal: (fun w w0 : Word => forall _ : inmonoid (union X V2) w, Rstar Word (Derive R2) w w0) u v *)
apply Derivestar_Ru.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	auto.

(* Goal: forall (u v w : Word) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) v, Rstar Word (Derive R2) v w) (_ : inmonoid (union X V2) u), Rstar Word (Derive R2) u w *)
	intros u0 v0 w Der_Ru inmon_v0_imp_Rstar_R2_v0 inmon_u0. 
(* Goal: Rstar Word (Derive R2) u0 w *)
	apply Rstar_R with v0.
(* Goal: Derive R2 u0 v0 *)
(* Goal: Rstar Word (Derive R2) v0 w *)
		prolog [ sym_inter isGram2 inter_union isGram4 inmon_Der_imp_Der_d2 ] 4.
		(*Apply inmon_Der_imp_Der_d2.
			Assumption.
			Assumption.
			Assumption.
			Apply isGram4 with S1;Assumption.
			Apply isGram4 with S2;Assumption.
			Apply inter_union.
				Apply isGram2 with R1 S1; Assumption.
				Apply sym_inter;Assumption.
			Assumption.
			Assumption.*)

(* Goal: Rstar Word (Derive R2) v0 w *)
		prolog [ inmon_Der_imp_inmon_d2 ] 3.
		(*Apply inmon_v0_imp_Rstar_R2_v0.
		Apply inmon_Der_imp_inmon_d2 with u0;Assumption.*)
Qed.


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.
(* Goal: forall (_ : not (dans S X)) (_ : not (dans S V1)) (_ : not (dans S V2)) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (u : Word) (_ : Derive Ru (cons S nil) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
intros N_dans_X N_dans_V1 N_dans_V2 G_1 G_2 u Derive_Ru.
(* Goal: or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
cut (Derive_inv Ru (cons S nil) u).
(* Goal: forall _ : Derive_inv Ru nil x, or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru nil x *)
(* Goal: Derive_inv Ru (cons S nil) u *)
unfold Derive_inv in |- *.
(* Goal: forall _ : False, or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru nil x *)
(* Goal: Derive_inv Ru (cons S nil) u *)
simpl in |- *.
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
intro temp; elim temp; clear temp; intro temp; elim temp; clear temp.

(* Goal: forall (x : Word) (_ : dans (couple S (word x)) Ru) (_ : @ex2 Word (fun v : Word => @eq Word (cons S v) (cons S nil)) (fun v : Word => @eq Word (Append x v) u)), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intros x dans_S_x_Ru temp.
(* Goal: or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	elim temp; clear temp.
(* Goal: forall (x0 : Word) (_ : @eq Word (cons S x0) (cons S nil)) (_ : @eq Word (Append x x0) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intros x0 egal_S_x0_S_nil egal_Append_x_x0_u.
(* Goal: or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) 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))). (**)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : @eq Elt (couple S (word (cons S2 nil))) (couple S (word x)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro egal_S.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	injection egal_S; auto.
	
(* Goal: forall _ : dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro dans_couple_add.
	cut
  (couple S (word (cons S2 nil)) = couple S (word x) :>Elt \/
   dans (couple S (word x)) (union R1 R2)). (***)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : @eq Elt (couple S (word (cons S2 nil))) (couple S (word x)), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro egal_S.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	injection egal_S; auto.
	
(* Goal: forall _ : dans (couple S (word x)) (union R1 R2), or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro dans_couple_union.	
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	cut (dans (couple S (word x)) R1 \/ dans (couple S (word x)) R2). (****)
(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : dans (couple S (word x)) R1, or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) R2, or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (dans (couple S (word x)) R1) (dans (couple S (word x)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intro dans_R1.
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: forall _ : dans (couple S (word x)) R2, or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (dans (couple S (word x)) R1) (dans (couple S (word x)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	absurd (dans S V1).
(* Goal: inmonoid X w *)
		assumption.
(* Goal: dans S V2 *)
(* Goal: or (dans (couple S (word x)) R1) (dans (couple S (word x)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
		prolog [ isGram4 Regles_inv1 ] 3.
		(*Apply Regles_inv1 with X R1 (word x) .
			Apply isGram4 with S1;Assumption.
			Assumption.*)

(* Goal: forall _ : dans (couple S (word x)) R2, or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (dans (couple S (word x)) R1) (dans (couple S (word x)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	intros dans_R2.
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (dans (couple S (word x)) R1) (dans (couple S (word x)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
	absurd (dans S V2).
(* Goal: inmonoid X w *)
		assumption.
(* Goal: dans S V2 *)
(* Goal: or (dans (couple S (word x)) R1) (dans (couple S (word x)) R2) *)
(* Goal: or (@eq Elt (couple S (word (cons S2 nil))) (couple S (word x))) (dans (couple S (word x)) (union R1 R2)) *)
(* Goal: or (@eq Elt (couple S (word (cons S1 nil))) (couple S (word x))) (dans (couple S (word x)) (add (couple S (word (cons S2 nil))) (union R1 R2))) *)
(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
		prolog [ isGram4 Regles_inv1 ] 3.
		(*Apply Regles_inv1 with X R2 (word x) .
			Apply isGram4 with S2;Assumption.
			Assumption.*)

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(****)auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(***)auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(**)auto.

(* Goal: @eq Word x u *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
replace x with (Append x nil).
(* Goal: @eq Word (Append x nil) u *)
(* Goal: @eq Word (Append x nil) x *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
replace nil with x0.
(* Goal: inmonoid X w *)
assumption.
(* Goal: inmonoid X w *)
apply cons_cons_inv2 with S S; assumption.
(* Goal: @eq Word (Append x nil) x *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
apply Append_w_nil.

(* Goal: forall (_ : not (dans S X)) (_ : not (dans S V1)) (_ : not (dans S V2)) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty), l_egal (LG X Vu Ru S) (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) *)
intros.
(* Goal: or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
cut (Derive_inv Ru nil x).
(* Goal: forall _ : Derive_inv Ru nil x, or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru nil x *)
(* Goal: Derive_inv Ru (cons S nil) u *)
unfold Derive_inv in |- *.
(* Goal: forall _ : False, or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru nil x *)
(* Goal: Derive_inv Ru (cons S nil) u *)
simpl in |- *.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
tauto.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
auto.
Qed.

Hint Resolve Gunion_disj_Derive1.



Lemma Gunion_disj_Derivestar_S :
 ~ 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 : Word,
 Derivestar Ru (cons S nil) u ->
 cons S nil = u :>Word \/
 Derivestar R1 (cons S1 nil) u \/ Derivestar R2 (cons S2 nil) u.
(* Goal: forall (_ : not (dans S X)) (_ : not (dans S V1)) (_ : not (dans S V2)) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty) (u : Word) (_ : Derivestar Ru (cons S nil) u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
intros N_dans_X N_dans_V1 N_dans_V2 G_1 G_2 inter_V1_V2_empty u Derivestar_Ru.

cut
 (cons S nil = u :>Word \/
  (exists2 w : Word, Derive Ru (cons S nil) w & Derivestar Ru w u)). (**)

(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
intro temp; elim temp; clear temp.
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	auto.

(* Goal: forall _ : @ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp.
(* Goal: forall (x : Word) (_ : Derive Ru (cons S nil) x) (_ : Derivestar Ru x u), or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intros x Der_Ru_cons_S_nil_x Derivestar_Ru_x_u.
(* Goal: or (@eq Word (cons S nil) u) (or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u)) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	right.
(* Goal: or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	cut (cons S1 nil = x :>Word \/ cons S2 nil = x :>Word). (***)

(* Goal: forall _ : or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x), or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 (cons S2 nil) u) *)
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
	intro temp; elim temp; clear temp; intro x_egal; rewrite x_egal.
(* Goal: or (Derivestar R1 x u) (Derivestar R2 (cons S2 nil) u) *)
(* Goal: or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 x u) *)
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
		apply or_introl.	
		apply Gunion_disj_Derivestar;
   [ auto
   | auto
   | auto
   | auto
   | auto
   | auto
   | auto
   | idtac ].
(* Goal: inmonoid (union X V1) x *)
(* Goal: or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 x u) *)
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
			rewrite <- x_egal; cut (dans S1 V1).
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
						auto.
(* Goal: dans S2 V2 *)
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
						prolog [ isGram3 ] 2.
						(*Apply isGram3 with X R1.
						Assumption.*)

(* Goal: or (Derivestar R1 (cons S1 nil) u) (Derivestar R2 x u) *)
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
		apply or_intror.	
		apply Gunion_disj_Derivestar2;
   [ auto
   | auto
   | auto
   | auto
   | auto
   | auto
   | auto
   | idtac ].
(* Goal: inmonoid (union X V2) x *)
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
			rewrite <- x_egal; cut (dans S2 V2).
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
						auto.
(* Goal: dans S2 V2 *)
(* Goal: or (@eq Word (cons S1 nil) x) (@eq Word (cons S2 nil) x) *)
(* Goal: or (@eq Word (cons S nil) u) (@ex2 Word (fun w : Word => Derive Ru (cons S nil) w) (fun w : Word => Derivestar Ru w u)) *)
						prolog [ isGram3 ] 2.
						(*Apply isGram3 with X R2.
						Assumption.*)

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	(***)auto.
	
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
(**)auto.
Qed.

Hint Resolve Gunion_disj_Derivestar_S.


Lemma Gunion_disj_LG_inclus1 :
 ~ dans S X ->
 ~ dans S V1 ->
 ~ dans S V2 ->
 isGram X V1 R1 S1 ->
 isGram X V2 R2 S2 ->
 inter V1 V2 empty ->
 l_inclus (LG X Vu Ru S) (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)).
(* Goal: forall (_ : not (dans S X)) (_ : not (dans S V1)) (_ : not (dans S V2)) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty), l_inclus (LG X Vu Ru S) (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) *)
intros N_dans_X N_dans_V1 N_dans_V2 G_1 G_2 inter_V1_V2_empty.
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
red in |- *.
(* Goal: forall (w : Word) (_ : LG X V2 R2 S2 w), LG X Vu Ru S w *)
unfold LG in |- *.
(* Goal: forall (w : Word) (_ : and (Derivestar Ru (cons S nil) w) (inmonoid X w)), lunion (fun w0 : Word => and (Derivestar R1 (cons S1 nil) w0) (inmonoid X w0)) (fun w0 : Word => and (Derivestar R2 (cons S2 nil) w0) (inmonoid X w0)) w *)
intros w temp; elim temp; clear temp; intros Der_Ru inmonoid_X_w.
(* Goal: lunion (fun w : Word => and (Derivestar R1 (cons S1 nil) w) (inmonoid X w)) (fun w : Word => and (Derivestar R2 (cons S2 nil) w) (inmonoid X w)) w *)
unfold lunion in |- *.
elimtype
 (cons S nil = w :>Word \/
  Derivestar R1 (cons S1 nil) w \/ Derivestar R2 (cons S2 nil) w). (**)
(* Goal: forall _ : @eq Word (cons S nil) w, or (and (Derivestar R1 (cons S1 nil) w) (inmonoid X w)) (and (Derivestar R2 (cons S2 nil) w) (inmonoid X w)) *)
(* Goal: forall _ : or (Derivestar R1 (cons S1 nil) w) (Derivestar R2 (cons S2 nil) w), or (and (Derivestar R1 (cons S1 nil) w) (inmonoid X w)) (and (Derivestar R2 (cons S2 nil) w) (inmonoid X w)) *)
(* Goal: or (@eq Word (cons S nil) w) (or (Derivestar R1 (cons S1 nil) w) (Derivestar R2 (cons S2 nil) w)) *)
	intro eg_cons_S_nil_w.
(* Goal: or (and (Derivestar R1 (cons S1 nil) w) (inmonoid X w)) (and (Derivestar R2 (cons S2 nil) w) (inmonoid X w)) *)
(* Goal: forall _ : or (Derivestar R1 (cons S1 nil) w) (Derivestar R2 (cons S2 nil) w), or (and (Derivestar R1 (cons S1 nil) w) (inmonoid X w)) (and (Derivestar R2 (cons S2 nil) w) (inmonoid X w)) *)
(* Goal: or (@eq Word (cons S nil) w) (or (Derivestar R1 (cons S1 nil) w) (Derivestar R2 (cons S2 nil) w)) *)
	absurd (dans S X).
(* Goal: inmonoid X w *)
		assumption.
(* Goal: dans S X *)
(* Goal: forall _ : or (Derivestar R1 (cons S1 nil) w) (Derivestar R2 (cons S2 nil) w), or (and (Derivestar R1 (cons S1 nil) w) (inmonoid X w)) (and (Derivestar R2 (cons S2 nil) w) (inmonoid X w)) *)
(* Goal: or (@eq Word (cons S nil) w) (or (Derivestar R1 (cons S1 nil) w) (Derivestar R2 (cons S2 nil) w)) *)
		apply inmonoid_cons_inv2 with nil.
(* Goal: inmonoid X w *)
		rewrite eg_cons_S_nil_w; assumption.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
	intro temp; elim temp; clear temp; auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
(**)auto.
Qed.

Lemma Gunion_disj_LG_inclus2 : l_inclus (LG X V1 R1 S1) (LG X Vu Ru S).
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
red in |- *.
(* Goal: forall (w : Word) (_ : LG X V2 R2 S2 w), LG X Vu Ru S w *)
unfold LG in |- *.
(* Goal: or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
intros w temp; elim temp; clear temp.
(* Goal: forall (_ : Derivestar R2 (cons S2 nil) w) (_ : inmonoid X w), and (Derivestar Ru (cons S nil) w) (inmonoid X w) *)
intros Der_Ru inmonoid_X_w.
(* Goal: forall _ : False, or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru nil x *)
(* Goal: Derive_inv Ru (cons S nil) u *)
unfold Ru in |- *; simpl in |- *.
(* Goal: and (Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) w) (inmonoid X w) *)
split.
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) w *)
(* Goal: inmonoid X w *)
	apply Derivestar_R with (cons S1 nil).
(* Goal: Derive (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) (cons S1 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S1 nil) w *)
(* Goal: inmonoid X w *)
		replace (cons S1 nil) with (Append (cons S1 nil) nil).
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
			auto.
			
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
			auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
		apply Derivestar_inclus with R1; auto.

(* Goal: inmonoid X w *)
assumption.
Qed.


Lemma Gunion_disj_LG_inclus3 : l_inclus (LG X V2 R2 S2) (LG X Vu Ru S).
(* Goal: l_inclus (LG X V2 R2 S2) (LG X Vu Ru S) *)
red in |- *.
(* Goal: forall (w : Word) (_ : LG X V2 R2 S2 w), LG X Vu Ru S w *)
unfold LG in |- *.
(* Goal: or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: forall (x : Word) (_ : Derive Ru nil x) (_ : @eq Word (cons S x) u), or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru (cons S nil) u *)
intros w temp; elim temp; clear temp.
(* Goal: forall (_ : Derivestar R2 (cons S2 nil) w) (_ : inmonoid X w), and (Derivestar Ru (cons S nil) w) (inmonoid X w) *)
intros Der_Ru inmonoid_X_w.
(* Goal: forall _ : False, or (@eq Word (cons S1 nil) u) (@eq Word (cons S2 nil) u) *)
(* Goal: Derive_inv Ru nil x *)
(* Goal: Derive_inv Ru (cons S nil) u *)
unfold Ru in |- *; simpl in |- *.
(* Goal: and (Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) w) (inmonoid X w) *)
split.
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) w *)
(* Goal: inmonoid X w *)
	apply Derivestar_R with (cons S2 nil).
(* Goal: Derive (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
		replace (cons S2 nil) with (Append (cons S2 nil) nil).
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
			auto.
			
(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
			auto.

(* Goal: @eq Word (Append (cons S2 nil) nil) (cons S2 nil) *)
(* Goal: Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S2 nil) w *)
(* Goal: inmonoid X w *)
		apply Derivestar_inclus with R2; auto.

(* Goal: inmonoid X w *)
assumption.
Qed.


Lemma Gunion_disj_LG_inclus4 :
 l_inclus (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) (LG X Vu Ru S).
(* Goal: l_inclus (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) (LG X Vu Ru S) *)
unfold l_inclus, lunion in |- *.
(* Goal: forall (w : Word) (_ : or (LG X V1 R1 S1 w) (LG X V2 R2 S2 w)), LG X Vu Ru S w *)
intros w temp; elim temp; clear temp; intro LG_w.
(* Goal: inmonoid X w *)
apply Gunion_disj_LG_inclus2; assumption.
(* Goal: inmonoid X w *)
apply Gunion_disj_LG_inclus3; assumption.
Qed.


Lemma Gunion_disj_LG :
 ~ dans S X ->
 ~ dans S V1 ->
 ~ dans S V2 ->
 isGram X V1 R1 S1 ->
 isGram X V2 R2 S2 ->
 inter V1 V2 empty ->
 l_egal (LG X Vu Ru S) (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)).
(* Goal: forall (_ : not (dans S X)) (_ : not (dans S V1)) (_ : not (dans S V2)) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty), l_egal (LG X Vu Ru S) (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) *)
intros.
(* Goal: and (Derivestar (add (couple S (word (cons S1 nil))) (add (couple S (word (cons S2 nil))) (union R1 R2))) (cons S nil) w) (inmonoid X w) *)
unfold l_egal in |- *; split.
(* Goal: inmonoid X w *)
apply Gunion_disj_LG_inclus1; assumption.
(* Goal: l_inclus (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) (LG X Vu Ru S) *)
exact Gunion_disj_LG_inclus4.
Qed.

End gram4.
