proposition: Lemma Der_cons_inv : forall (x : Elt) (u v : Word), dans x X -> Derivestar_P_A_2 (cons x u, v) (nil, nil) -> ex2 (fun v2 : Word => v = cons x v2) (fun v2 : Word => Derivestar_P_A_2 (u, v2) (nil, nil)).
proof: Proof. intros x u v dans_x_X Der_star. elimtype ((cons x u, v) = (nil, nil) \/ ex2 (fun z : Conf => Derive_P_A_2 (cons x u, v) z) (fun z : Conf => Rstar (Word * Word) Derive_P_A_2 z (nil, nil))). intro eg. absurd (cons x u = nil). discriminate. change (fst (cons x u, v) = fst (nil, nil)) in |- *. apply (f_equal (fst (A:=Word) (B:=Word))). assumption. intro temp; elim temp; clear temp; intros z Der Der_star_2. cut (Derive_P_A_2_nind (cons x u, v) z). unfold Derive_P_A_2_nind in |- *. intro temp; elim temp; clear temp; intro temp; elim temp; clear temp. simpl in |- *. intros x0 dans_x0_X temp; elim temp; clear temp. intros eg_cons_x_x0 eg_v_cons. exists (snd z). replace x with x0. trivial. apply cons_cons_inv1 with (fst z) u. auto. unfold Derivestar_P_A_2 in |- *. replace u with (fst z). cut (Rstar (Word * Word) Derive_P_A_2 z (nil, nil)). elim z. auto. assumption. apply cons_cons_inv2 with x0 x. auto. simpl in |- *. intros x0 temp; elim temp; clear temp; intros w eg temp; elim temp; clear temp. intros u0 dans_couple. absurd (dans x0 V). apply inter_dans with X. exact (isGram2 X V R S' Gram). replace x0 with x. trivial. apply cons_cons_inv1 with u w. auto. apply Regles_inv1 with X R (word u0). exact Regles_X_V_R. assumption. apply Derive_P_A_2_inv. assumption. apply Rstar_inv. assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata