proposition: Lemma Deriveg_imp_Deriveg_App : forall x y : Word, Deriveg 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 => Deriveg X R v w).
proof: Proof. intros x y Derg. elim Derg. intros u0 v0 A dans_A_u0_R u v eg_App. elimtype (u = nil \/ (exists w : Word, (exists x : Elt, u = cons x w))). intros u_eg. exists (Append u0 v0). rewrite u_eg. trivial. replace v with (cons A v0). apply Deriveg1; assumption. replace v with (Append u v). auto. rewrite u_eg. trivial. intro temp; elim temp; clear temp. intros w temp; elim temp; clear temp. intros x0 u_eg inmon_u. absurd (dans x0 V). apply inter_dans with X. apply isGram2 with R S'. exact Gram. apply inmonoid_cons_inv2 with w. rewrite <- u_eg. assumption. replace x0 with A. apply Regles_inv1 with X R (word u0). exact Regles_X_V_R. assumption. apply cons_cons_inv1 with v0 (Append w v). change (cons A v0 = Append (cons x0 w) v) in |- *. rewrite <- u_eg. auto. clear eg_App. generalize u; clear u; simple induction u. auto. intros x0 w hyp. apply or_intror. exists w. exists x0. trivial. intros u0 v0 x0 dans_x0_X Derg_u_v Hyp u v. elimtype (u = nil \/ (exists w : Word, (exists x : Elt, u = cons x w))). intro eg_u. rewrite eg_u. intros App_eg inmon_nil. exists (cons x0 v0). trivial. replace v with (cons x0 u0). apply Deriveg2. assumption. assumption. intro temp; elim temp; clear temp. intros w temp; elim temp; clear temp. intros x1 u_eg. rewrite u_eg. intros App_cons_eg inmonoid_X_cons_x1_w. elimtype (ex2 (fun w1 : Word => Append w w1 = v0) (fun w1 : Word => Deriveg X R v w1)). intros w0 App_eg Der_v_w0. exists w0. change (cons x1 (Append w w0) = cons x0 v0) in |- *. apply cons_cons. apply cons_cons_inv1 with (Append w v) u0. assumption. assumption. assumption. apply Hyp. apply cons_cons_inv2 with x1 x0. assumption. apply inmonoid_cons_inv with x1. assumption. generalize u; clear u; simple induction u. auto. intros x2 w hyp. apply or_intror. exists w. exists x2. trivial. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata