proposition: Lemma Trans : Transition X P d.
proof: Proof. red in |- *. intros x dans_x_d. elimtype (dans x (map f_R_d R) \/ dans x (map f_X_d X)). intros dans_x. elimtype (exists y : Elt, dans y R /\ x = f_R_d y). intros y temp; elim temp; clear temp. unfold f_R_d in |- *. intros dans_y_R eg_x_f_y. exists (cons (first y) nil). apply inmonoid_cons. trivial. elim (Regles_X_V_R y dans_y_R). intros f_y dans_f_y_V temp; elim temp; clear temp. intros u eg_y inmono_u. rewrite eg_y. unfold first in |- *. unfold P in |- *. auto. exists (eps X). auto. exists (word_inv (second y)). elim (Regles_X_V_R y dans_y_R). intros f_y dans_f_y_V temp; elim temp; clear temp. intros u eg_y inmono_u. rewrite eg_y. unfold second in |- *. unfold word_inv in |- *. assumption. elim (Regles_X_V_R y dans_y_R). intros f_y dans_f_y_V temp; elim temp; clear temp. intros u eg_y inmono_u. replace (word (word_inv (second y))) with (second y). assumption. replace (second y) with (word u). apply refl_equal. rewrite eg_y. apply refl_equal. apply dans_map. assumption. intros dans_x. elimtype (exists y : Elt, dans y X /\ x = f_X_d y). intros y temp; elim temp; clear temp. unfold f_X_d in |- *. intros dans_y_X eg_x_f_y. exists (cons y nil). apply inmonoid_cons. trivial. unfold P in |- *. auto. exists y. auto. exists nil. trivial. assumption. apply dans_map. assumption. auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata