proposition: Lemma chemin_restriction_1 : forall (q1 qd1 qa1 d1 q2 qa2 d2 : Ensf) (w : Word) (e1 e2 : Elt), automate q1 qd1 qa1 d1 -> chemin e1 e2 (union_disj q1 q2) (union (injg_d1 q1 d1) (injd_d2 q2 d2)) w -> dans e1 (map injgauche q1) -> dans e2 (union_disj qa1 qa2) -> chemin (first e1) (first e2) q1 d1 w /\ dans e2 (map injgauche qa1).
proof: Proof. intros q1 qd1 qa1 d1 q2 qa2 d2. simple induction w. intros e1 e2 H H0 H1 H2. cut (Chemin e1 e2 (union_disj q1 q2) (union (injg_d1 q1 d1) (injd_d2 q2 d2)) nil); auto. intro. cut (dans e1 (union_disj q1 q2) /\ e1 = e2 :>Elt); auto. intro Ht; elim Ht; clear Ht; intros H4 H5. split. apply chemin_nil. 2: apply (f_equal (A:=Elt) (B:=Elt)); auto. apply dans_map_injg; auto. unfold union_disj in H2. cut (dans e2 (map injgauche qa1) \/ dans e2 (map injdroite qa2)); auto. intro Ht; elim Ht; clear Ht. auto. intro. absurd (dans e2 (map injdroite qa2)); auto. rewrite <- H5. apply absurd_injg_injd with q1; auto. intros x w0 H e1 e2 H0 H1 H2 H3. cut (Chemin e1 e2 (union_disj q1 q2) (union (injg_d1 q1 d1) (injd_d2 q2 d2)) (cons x w0)); auto. intro. cut (exists e : Elt, chemin e e2 (union_disj q1 q2) (union (injg_d1 q1 d1) (injd_d2 q2 d2)) w0 /\ dans e1 (union_disj q1 q2) /\ dans x alph /\ dans (couple e1 (couple x e)) (union (injg_d1 q1 d1) (injd_d2 q2 d2))); auto. intro Ht; elim Ht; clear Ht. intros e Ht; elim Ht; clear Ht. intros H5 Ht; elim Ht; clear Ht. intros H6 Ht; elim Ht; clear Ht; intros H7 H8. cut (dans e (map injgauche q1)). 2: apply transition_dans_d1 with d1 q2 d2 e1 x; auto. intro. cut (chemin (first e) (first e2) q1 d1 w0 /\ dans e2 (map injgauche qa1)); auto. intro Ht; elim Ht; clear Ht; intros H10 H11. split; auto. apply chemin_cons with (first e); auto. apply dans_map_injg; auto. apply restriction_transition_d1 with q1 q2 d2; auto. Qed.
imports: Ensf Max Words Dec Reg Rat