proposition: Lemma Derivestar_P_A_2_imp_Derivestar_P_A_3 : forall x y : Conf, Derivestar_P_A_2 x y -> forall s : Word, exists s2 : Word, Derivestar_P_A_3 (s, x) (s2, y).
proof: Proof. unfold Derivestar_P_A_2, Rstar, Derivestar_P_A_3 in |- *. intros x y Der_star. pattern x, y in |- *. apply Der_star. intros; exists s. apply Rstar_reflexive. intros u v w Der_u_v Ex_v_w s. elimtype (exists s2 : Word, Derive_P_A_3 (s, u) (s2, v)). intros s1 Der_3_s_u_s1_v. elim (Ex_v_w s1). intros s2 Rstar_s1_v_s2_w. exists s2. apply Rstar_R with (s1, v); trivial. apply Derive_P_A_2_imp_Derive_P_A_3; assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata