proposition: 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.
proof: Proof. 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)). intro temp; elim temp; clear temp. auto. intro temp; elim temp; clear temp. intros x Der_Ru_cons_S_nil_x Derivestar_Ru_x_u. right. cut (cons S1 nil = x :>Word \/ cons S2 nil = x :>Word). intro temp; elim temp; clear temp; intro x_egal; rewrite x_egal. apply or_introl. apply Gunion_disj_Derivestar; [ auto | auto | auto | auto | auto | auto | auto | idtac ]. rewrite <- x_egal; cut (dans S1 V1). auto. prolog [ isGram3 ] 2. apply or_intror. apply Gunion_disj_Derivestar2; [ auto | auto | auto | auto | auto | auto | auto | idtac ]. rewrite <- x_egal; cut (dans S2 V2). auto. prolog [ isGram3 ] 2. auto. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3