proposition: Lemma Derivestar_P_A_imp_Derivestar_P_A_2 : forall x y : Word * Word, Derivestar_P_A X d x y -> Derivestar_P_A_2 x y.
proof: Proof. unfold Derivestar_P_A, Rstar, Derivestar_P_A_2 in |- *. intros x y Der_star. pattern x, y in |- *. apply Der_star. intros. apply Rstar_reflexive. intros u v w Deri_u_v Rstar_v_w. apply Rstar_R with v; auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata