proposition: Lemma automateA_automate : forall q qd qaA dA : Ensf, automate_A q qd qaA dA -> automate q qd (sync_qa q qaA dA) (sync_d q dA).
proof: Proof. intros. elim H. intros H1 H2; elim H2; clear H2; intros H2 H3. red in |- *. split. unfold sync_qa in |- *. apply union_inclus; auto. apply inclus_tq. split; auto. unfold sync_d in |- *. apply inclus_tq. Qed.
imports: Ensf Max Words Dec