proposition: Lemma reconnait_reconnaitA : forall (q qd qaA dA : Ensf) (w : Word), automate_A q qd qaA dA -> reconnait q qd (sync_qa q qaA dA) (sync_d q dA) w -> reconnait_A q qd qaA dA w.
proof: Proof. intros q qd qaA dA w H_aut. unfold reconnait in |- *. intro Ht; elim Ht; clear Ht. intros H Ht; elim Ht; clear Ht. intros e1 Ht; elim Ht; clear Ht. intros e2 Ht; elim Ht; clear Ht. intros H0 Ht; elim Ht; clear Ht. intros H1 H2. cut (dans e2 (union qaA (tq (fun e : Elt => exists e' : Elt, dans e' qaA /\ chemin_A q dA e e' nil) q))); auto. intro H3. 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 H4. unfold reconnait_A in |- *. split; auto. exists e1. clear H3; elim H4. intro. exists e2. split; auto. split; auto. apply (chemin_cheminA q qd qaA dA H_aut); 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 => exists e' : Elt, dans e' qaA /\ chemin_A q dA e e' nil); auto. intro Ht; elim Ht; clear Ht. intros H5 Ht; elim Ht; clear Ht. intros e2' Ht; elim Ht; clear Ht. intros H6 H7. exists e2'. split; auto. split; auto. cut (chemin_A q dA e1 e2 w). 2: apply (chemin_cheminA q qd qaA dA H_aut); auto. intro. replace w with (Append w nil). apply chemin_Append with e2; auto. apply Append_w_nil. Qed.
imports: Ensf Max Words Dec