proposition: Lemma Derive_P_A_2_imp_Derive_P_A : forall x y : Word * Word, Derive_P_A_2 x y -> Derive_P_A X d x y.
proof: Proof. intros x y Der. elim Der. intros w u x0 dans_x0_X. replace (cons x0 w) with (Append (cons x0 nil) w). pattern w at 2 in |- *. replace w with (Append nil w). apply Derive_cons. assumption. unfold d in |- *. apply union_d. change (dans (f_X_d x0) (map f_X_d X)) in |- *. apply dans_map_inv. assumption. trivial. trivial. intros v w u x0 dans_couple. replace (cons x0 w) with (Append (cons x0 nil) w). apply Derive_eps. unfold d in |- *. apply union_g. replace (couple (word (cons x0 nil)) (couple (eps X) (word u))) with (f_R_d (couple x0 (word u))). apply dans_map_inv. assumption. unfold f_R_d in |- *. trivial. trivial. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata