proposition: Lemma legal_false_D : forall (c0 : Config) (s0 : Site), legal c0 -> rt c0 s0 = false -> D_queue (bm c0 s0 owner).
proof: Proof. intros c0 s0 H; elim H. intro; apply D_init. simple induction t; unfold transition in |- *; intros. apply copy_trans_D; auto. apply rdec_trans_D; auto. apply rinc_trans_D. apply (not_owner_first_inc c s3 s1 owner); auto. auto. apply rcop1_trans_D; auto. apply rcop2_trans_D; auto. apply rcop3_trans_D; auto. apply del_trans_D; auto. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc