proposition: Lemma reconnaitA_reconnait : forall (q qd qaA dA : Ensf) (w : Word), automate_A q qd qaA dA -> reconnait_A q qd qaA dA w -> reconnait q qd (sync_qa q qaA dA) (sync_d q dA) w.
proof: Proof. intros q qd qaA dA w H_aut. unfold reconnait_A in |- *. intro H; elim H; clear H. intros H1 H; elim H; clear H. intros e1 H; elim H; clear H. intros e2 H; elim H; clear H. intros H2 H; elim H; clear H; intros H3 H4. unfold reconnait in |- *. split; auto. exists e1. cut (exists e2' : Elt, chemin e1 e2' q (sync_d q dA) w /\ dans e2' (sync_qa q qaA dA)). 2: apply (cheminA_chemin q qd qaA dA H_aut w e1 e2); auto. intro Ht; elim Ht; clear Ht. intros e2' Ht; elim Ht; clear Ht. intros H5 H6. exists e2'. auto. Qed.
imports: Ensf Max Words Dec