proposition: Lemma Derive_P_A_imp_Derive_P_A_2 : forall x y : Word * Word, Derive_P_A X d x y -> Derive_P_A_2 x y.
proof: Proof. unfold d in |- *. intros x y Der. elim Der. intros w w1 w2 u x0 dans_x0_X dans_couple_d. elimtype (dans (couple (word w1) (couple x0 (word w2))) (map f_R_d R) \/ dans (couple (word w1) (couple x0 (word w2))) (map f_X_d X)). intros dans_couple. absurd (dans (eps X) X). apply not_dans_X_eps. replace (eps X) with x0. assumption. elimtype (exists r : Elt, dans r R /\ couple (word w1) (couple x0 (word w2)) = f_R_d r). intros r temp; elim temp; clear temp; intros dans_r_R. unfold f_R_d in |- *. intro eg. apply couple_couple_inv1 with (word w2) (second r). apply couple_couple_inv2 with (word w1) (word (cons (first r) nil)). assumption. apply dans_map. assumption. intros dans_couple. elimtype (exists r : Elt, dans r X /\ couple (word w1) (couple x0 (word w2)) = f_X_d r). intros r temp; elim temp; clear temp; intros dans_r_X eg. replace w1 with (cons x0 nil). replace w2 with nil. simpl in |- *. replace (Append nil w) with w. replace (Append (cons x0 nil) w) with (cons x0 w). apply Derive_X. assumption. trivial. trivial. apply word_word_inv. apply couple_couple_inv2 with r x0. apply couple_couple_inv2 with (word (cons r nil)) (word w1). auto. replace x0 with r. apply word_word_inv. apply couple_couple_inv1 with (couple r (word nil)) (couple x0 (word w2)). auto. apply couple_couple_inv1 with (word nil) (word w2). apply couple_couple_inv2 with (word (cons r nil)) (word w1). auto. apply dans_map. assumption. auto. unfold d in |- *. intros w w1 w2 u dans_couple_d. elimtype (dans (couple (word w1) (couple (eps X) (word w2))) (map f_R_d R) \/ dans (couple (word w1) (couple (eps X) (word w2))) (map f_X_d X)). intros dans_couple. elimtype (exists r : Elt, dans r R /\ couple (word w1) (couple (eps X) (word w2)) = f_R_d r). intros r temp; elim temp; clear temp; intros dans_r_R eg. replace w1 with (cons (first r) nil). replace (Append (cons (first r) nil) w) with (cons (first r) w). apply Derive_V. replace (word w2) with (second r). elimtype (ex2 (fun A : Elt => dans A V) (fun A : Elt => ex2 (fun B : Word => r = couple A (word B)) (fun B : Word => inmonoid (union X V) B))). intros A dans_A_V temp; elim temp; clear temp; intros B eg_r inmon_B. rewrite eg_r. replace (first (couple A (word B))) with A. replace (second (couple A (word B))) with (word B). rewrite <- eg_r. assumption. trivial. trivial. apply Regles_X_V_R. assumption. apply couple_couple_inv2 with (eps X) (eps X). apply couple_couple_inv2 with (word (cons (first r) nil)) (word w1). auto. trivial. apply word_word_inv. apply couple_couple_inv1 with (couple (eps X) (second r)) (couple (eps X) (word w2)). auto. apply dans_map. assumption. intro dans_couple. elimtype (exists r : Elt, dans r X /\ couple (word w1) (couple (eps X) (word w2)) = f_X_d r). intros r temp; elim temp; clear temp; intros dans_r_X eg. absurd (dans (eps X) X). apply not_dans_X_eps. replace (eps X) with r. assumption. apply couple_couple_inv1 with (word nil) (word w2). apply couple_couple_inv2 with (word (cons r nil)) (word w1). auto. apply dans_map. assumption. auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata