proposition: Lemma Conserve_App_s_u : forall s1 s2 u1 u2 v1 v2 : Word, Derive_P_A_3 (s1, (u1, v1)) (s2, (u2, v2)) -> Append s1 v1 = Append s2 v2.
proof: Proof. intros s1 s2 u1 u2 v1 v2 Derive_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 |- *. elim Derive_P_A_3_s1_v1_s2_v2; simpl in |- *. intros w u s x dans_x_X. replace (cons x u) with (Append (cons x nil) u); trivial. auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata