proposition: Lemma cheminA_chemin : forall q qd qaA dA : Ensf, automate_A q qd qaA dA -> forall (w : Word) (e1 e2 : Elt), chemin_A q dA e1 e2 w -> dans e2 qaA -> exists e2' : Elt, chemin e1 e2' q (sync_d q dA) w /\ dans e2' (sync_qa q qaA dA).
proof: Proof. intros q qd qaA dA H_aut w. cut (inclus qaA (sync_qa q qaA dA)). 2: apply inclus_qaA_qa. intro H0. intros e1 e2 H1. elim H1. intros e0 e3 H H2 H3. exists e0. split. apply chemin_nil; auto. rewrite H2. apply dans_trans with qaA; auto. intros. cut (exists e2' : Elt, chemin e e2' q (sync_d q dA) w0 /\ dans e2' (sync_qa q qaA dA)); auto. intro Ht; elim Ht; clear Ht. intros e2' Ht; elim Ht; clear Ht. intros H7 H8. exists e2'. split; auto. apply chemin_cons with e; auto. cut (dans e q). 2: apply (dans_e1_q q (sync_d q dA) w0 e e2'); auto. intro dans_e_q. apply trans_dA_d; auto. intros. cut (exists e2' : Elt, chemin e e2' q (sync_d q dA) w0 /\ dans e2' (sync_qa q qaA dA)); auto. intro Ht; elim Ht; clear Ht. intros e9 Ht; elim Ht; clear Ht. intros H6 H7. apply (epsilon_chemin q qaA dA w0 e0 e e9); auto. Qed.
imports: Ensf Max Words Dec