proposition: Lemma Derive_P_A_3_imp_Derivegstar : forall x y x' y' s s' : Word, Derive_P_A_3 (s, (x, y)) (s', (x', y')) -> inmonoid X s -> Derivegstar X R (Append s x) (Append s' x').
proof: Proof. intros x y x' y' s s' Der. change ((fun a a' : Word * Conf => inmonoid X (fst a) -> Derivegstar X R (Append (fst a) (fst (snd a))) (Append (fst a') (fst (snd a')))) (s, (x, y)) (s', (x', y'))) in |- *. unfold Derivegstar in |- *. elim Der; simpl in |- *. intros w u s0 x0 dans_x0_X inmon_s. replace (Append (Append s0 (cons x0 nil)) w) with (Append s0 (Append (cons x0 nil) w)). apply Rstar_reflexive. auto. intros v w u s0 x0 dans_couple_x0_u_R inmon_s. apply Rstar_R with (Append s0 (Append u w)). apply Deriveg_imp_Deriveg_App_2. assumption. apply Deriveg1. assumption. apply Rstar_reflexive. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata