proposition: Lemma chemin_cheminA : forall q qd qaA dA : Ensf, automate_A q qd qaA dA -> forall (w : Word) (e1 e2 : Elt), chemin e1 e2 q (sync_d q dA) w -> chemin_A q dA e1 e2 w.
proof: Proof. intros q qd qaA dA H_aut. simple induction w. intros. cut (Chemin e1 e2 q (sync_d q dA) nil); auto. intro. cut (dans e1 q /\ e1 = e2 :>Elt); auto. intro Ht; elim Ht; clear Ht. intros; apply chemin_A_nil; auto. intros x w0 H e1 e2 H0. cut (Chemin e1 e2 q (sync_d q dA) (cons x w0)); auto. intro H1. cut (exists e : Elt, chemin e e2 q (sync_d q dA) w0 /\ dans e1 q /\ dans x alph /\ dans (couple e1 (couple x e)) (sync_d q dA)); auto. intro Ht; elim Ht; clear Ht. intros e Ht; elim Ht; clear Ht. intros H2 Ht; elim Ht; clear Ht. intros H3 H4. cut (chemin_A q dA e e2 w0); auto. intro. elim H4; clear H4; intros H4 H6. cut (chemin_A q dA e1 e (cons x nil)). 2: apply sync_d_def2; auto. intro. replace (cons x w0) with (Append (cons x nil) w0); auto. apply chemin_Append with e; auto. Qed.
imports: Ensf Max Words Dec