proposition: Lemma Derivegstar_imp_Derivestar_P_A_2 : forall x y : Word, Derivegstar X R x y -> inmonoid X y -> Derivestar_P_A_2 (x, y) (nil, nil).
proof: Proof. unfold Derivegstar, Rstar in |- *. intros x y Der_star. pattern x, y in |- *. apply Der_star. auto. intros u v w Derg_u_v. generalize w. elim Derg_u_v. intros u0 v0 A dans_couple w0 Hyp inmon_w0. unfold Derivestar_P_A_2 in |- *. apply Rstar_R with (Append u0 v0, w0). apply Derive_V. assumption. apply Hyp; assumption. intros u0 v0 x0 dans_x0_v0 Der_u0_v0 Hyp1 w0 Hyp2 inmon_w0. elimtype (ex2 (fun v2 : Word => w0 = cons x0 v2) (fun v2 : Word => Derivestar_P_A_2 (v0, v2) (nil, nil))). intros x1 w0_eg_cons Derivestar_v0_x1. rewrite w0_eg_cons. unfold Derivestar_P_A_2 in |- *. apply Rstar_R with (u0, x1). apply Derive_X. assumption. apply Hyp1. auto. apply inmonoid_cons_inv with x0. rewrite <- w0_eg_cons. assumption. apply Der_cons_inv. assumption. exact (Hyp2 inmon_w0). Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata