proposition: Lemma Deriveg_imp_Deriveg_cut : forall x y : Word, Deriveg X R x y -> ex2 (fun w : Word => Append (cut1 x) w = y) (fun w : Word => Deriveg X R (cut2 x) w).
proof: Proof. intros x y Der. elim Der. intros. replace (cut1 (cons A v)) with nil. exists (Append u v). trivial. replace (cut2 (cons A v)) with (cons A v). apply Deriveg1. assumption. apply sym_equal. apply cut2_cons_N. apply inter_dans with V. apply sym_inter. apply isGram2 with R S'. exact Gram. apply Regles_inv1 with X R (word u). apply isGram4 with S'. exact Gram. assumption. unfold cut1, cut in |- *. elim (cut_spec (cons A v)). intros a p. elim p. intros b temp; elim temp; clear temp. intros inmon_a temp; elim temp; clear temp. intros App_eg spec_or. cut (inmonoid X a). cut (Append a b = cons A v). clear App_eg inmon_a p. generalize a; clear a; simple induction a. auto. intros x0 w Hyp App inmon. absurd (dans A X). intros. apply inter_dans with V. apply sym_inter. apply isGram2 with R S'. exact Gram. apply Regles_inv1 with X R (word u). apply isGram4 with S'. exact Gram. assumption. apply inmonoid_cons_inv2 with w. replace A with x0. assumption. apply cons_cons_inv1 with (Append w b) v. assumption. assumption. assumption. intros u v x0 dans_x0_X Deriveg_X_R_u_v temp. elim temp; clear temp. intros w eg_App_cut Der_g_cut2. exists w. replace (cut1 (cons x0 u)) with (cons x0 (cut1 u)). unfold Append in |- *. simpl in |- *. apply cons_cons; trivial. apply sym_equal. apply cut1_cons. assumption. replace (cut2 (cons x0 u)) with (cut2 u). assumption. apply sym_equal. apply cut2_cons. assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata