proposition: Lemma epsilon_chemin : forall (q qaA dA : Ensf) (w : Word) (e1 e e2 : Elt), chemin e e2 q (sync_d q dA) w -> dans (couple e1 (couple epsilon e)) dA -> dans e2 (sync_qa q qaA dA) -> dans e1 q -> exists e2' : Elt, chemin e1 e2' q (sync_d q dA) w /\ dans e2' (sync_qa q qaA dA).
proof: Proof. intros q qaA dA. simple induction w. intros. exists e1. split. auto. cut (Chemin e e2 q (sync_d q dA) nil); auto. intro H3. cut (dans e q /\ e = e2 :>Elt); auto. intro Ht; elim Ht; clear Ht. intros H4 H5. cut (chemin_A q dA e e2 nil); auto. cut (chemin_A q dA e1 e2 nil). 2: apply chemin_A_epsilon with e; auto. intros. unfold sync_qa in H1. cut (dans e2 qaA \/ dans e2 (tq (fun e : Elt => exists e' : Elt, dans e' qaA /\ chemin_A q dA e e' nil) q)). 2: apply dans_union; auto. intro Ht; elim Ht; clear Ht. intro; apply nouvx_dans_qa; auto. exists e2; auto. intro. cut (dans e2 q /\ (fun e : Elt => exists e' : Elt, dans e' qaA /\ chemin_A q dA e e' nil) e2). 2: apply dans_tq_imp with (f := fun e : Elt => ex (fun e' : Elt => dans e' qaA /\ chemin_A q dA e e' nil)); assumption. intro Ht; elim Ht; clear Ht. intros H9 Ht; elim Ht; clear Ht. intros e3 Ht; elim Ht; clear Ht. intros H10 H11. cut (chemin_A q dA e e3 nil); auto. 2: rewrite H5; auto. intro H12. cut (chemin_A q dA e1 e3 nil). 2: apply chemin_A_epsilon with e; auto. intro; apply nouvx_dans_qa; auto. exists e3; auto. intros x w0 H e1 e e2 H0 H1 H2 H3. cut (Chemin e e2 q (sync_d q dA) (cons x w0)); auto. intro. cut (exists e22 : Elt, chemin e22 e2 q (sync_d q dA) w0 /\ dans e q /\ dans x alph /\ dans (couple e (couple x e22)) (sync_d q dA)); auto. intro Ht; elim Ht; clear Ht. intros e22 Ht; elim Ht; clear Ht. intros H5 Ht; elim Ht; clear Ht. intros H6 Ht; elim Ht; clear Ht; intros H7 H8. exists e2. split; auto. cut (chemin_A q dA e e22 (cons x nil)). 2: apply sync_d_def2; auto. intro. cut (chemin_A q dA e1 e22 (cons x nil)). 2: apply chemin_A_epsilon with e; auto. intro. cut (dans (couple e1 (couple x e22)) (sync_d q dA)). 2: apply sync_d_def; auto. intro. apply chemin_cons with e22; auto. Qed.
imports: Ensf Max Words Dec