proposition: Lemma async_is_sync : forall q qd qaA dA : Ensf, automate_A q qd qaA dA -> exists d : Ensf, (exists qa : Ensf, automate q qd qa d /\ eqwordset (reconnait_A q qd qaA dA) (reconnait q qd qa d)).
proof: Proof. intros q qd qaA dA H. exists (sync_d q dA). exists (sync_qa q qaA dA). split. apply automateA_automate; auto. unfold eqwordset in |- *. split. intro. apply reconnaitA_reconnait; auto. intro. apply reconnait_reconnaitA; auto. Qed.
imports: Ensf Max Words Dec