proposition: Lemma Derivegstar_imp_Der_inmon : forall x y : Word, Derivegstar X R x y -> forall u v : Word, Append u v = x -> inmonoid X u -> ex2 (fun w : Word => Append u w = y) (fun w : Word => Derivegstar X R v w).
proof: Proof. unfold Derivegstar in |- *. intros x y Der_star. unfold Rstar in Der_star. pattern x, y in |- *. apply Der_star. intros; exists v. assumption. apply Rstar_reflexive. intros u v w Der_u_v Hyp u0 v0 App_eg inmon_u0. elimtype (ex2 (fun w1 : Word => Append u0 w1 = v) (fun w1 : Word => Deriveg X R v0 w1)). intros w0 App_eg_u0_w0 Deriveg_v0_x0. elimtype (ex2 (fun w1 : Word => Append u0 w1 = w) (fun w1 : Word => Rstar Word (Deriveg X R) w0 w1)). intros w1 App_eg_u0_w1_w Rstar_Der. exists w1. assumption. apply Rstar_R with w0. assumption. assumption. apply Hyp; assumption. apply Deriveg_imp_Deriveg_App with u; assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata