proposition: Lemma isregular_A_isregular : forall l : wordset, isregular_A l -> isregular l.
proof: Proof. unfold isregular_A in |- *. intros l Ht; elim Ht; clear Ht. intros q Ht; elim Ht; clear Ht. intros qd Ht; elim Ht; clear Ht. intros qaA Ht; elim Ht; clear Ht. intros dA Ht; elim Ht; clear Ht. intros. cut (exists d : Ensf, (exists qa : Ensf, automate q qd qa d /\ eqwordset (reconnait_A q qd qaA dA) (reconnait q qd qa d))). 2: apply async_is_sync; auto. intro Ht; elim Ht; clear Ht. intros d Ht; elim Ht; clear Ht. intros qa Ht; elim Ht; clear Ht. intros. unfold isregular in |- *. exists q. exists qd. exists qa. exists d. split; auto. apply eqwordset_trans with (reconnait_A q qd qaA dA); auto. apply eqwordset_sym; auto. Qed.
imports: Ensf Max Words Dec