proposition: Lemma Derivestar_P_A_3_imp_Derivegstar : forall x y x' y' s s' : Word, Derivestar_P_A_3 (s, (x, y)) (s', (x', y')) -> inmonoid X s -> Derivegstar X R (Append s x) (Append s' x').
proof: Proof. unfold Derivestar_P_A_3, Rstar in |- *. intros x y x' y' s s' Der_star. 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 |- *. apply Der_star; unfold Derivegstar in |- *. intros. apply Rstar_reflexive. intros u v w. elim u. intros u1 uc. elim uc. intros u2 u3. elim v. intros v1 vc. elim vc. intros v2 v3. simpl in |- *. intros Der_3_u_v Hyp inmon_u1. apply Rstar_transitive with (Append v1 v2). change (Derivegstar X R (Append u1 u2) (Append v1 v2)) in |- *. apply Derive_P_A_3_imp_Derivegstar with u3 v3. assumption. assumption. apply Hyp. apply Derive_P_A_3_conserve_inmonoid_s with u2 u3 v2 v3 u1. assumption. assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata