proposition: Lemma Derisvestar_P_A_3_conserve : forall s1 s2 u1 u2 v1 v2 : Word, Derivestar_P_A_3 (s1, (u1, v1)) (s2, (u2, v2)) -> Append s1 v1 = Append s2 v2.
proof: Proof. unfold Derivestar_P_A_3, Rstar in |- *. intros s1 s2 u1 u2 v1 v2 Derivestar_P_A_3_s1_v1_s2_v2. change ((fun a b : Word * Conf => Append (fst a) (snd (snd a)) = Append (fst b) (snd (snd b))) (s1, (u1, v1)) (s2, (u2, v2))) in |- *. apply Derivestar_P_A_3_s1_v1_s2_v2. trivial. intros u v w. elim u. intros uu1 uuc. elim uuc. intros uu2 uu3. elim v. intros vv1 vvc. elim vvc. intros vv2 vv3. simpl in |- *. intros Der eg1. rewrite <- eg1. apply Conserve_App_s_u with uu2 vv2. assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata