proposition: Lemma false_rt_D_queue : forall (c : Config) (s : Site), legal c -> rt c s = false -> D_queue (bm c s owner).
proof: Proof. intros c s H; elim H. simpl in |- *. intro. apply D_empty. simple induction t; simpl in |- *; intros. apply D_post_elsewhere; auto. apply D_collect; auto. apply D_post_elsewhere. right. apply (not_owner_inc3 c0 s1 owner H0 s3). apply first_in. auto. apply D_collect. auto. case (eq_queue_dec s2 s s1 owner); intros; simpl in |- *. decompose [and] a. rewrite H3; rewrite H4. apply D_post_dec. apply D_post_elsewhere. auto. apply D_collect; auto. case (eq_site_dec s s2); intro. generalize H2; rewrite e1; unfold Set_rec_table in |- *; rewrite that_site. intro; discriminate. apply D_collect. apply H1. generalize H2; unfold Set_rec_table in |- *; rewrite other_site; auto. case (eq_site_dec s s2); intro. generalize H2; rewrite e1; unfold Set_rec_table in |- *; rewrite that_site; intro; discriminate. apply D_post_elsewhere; auto. apply D_collect; auto. apply H1; generalize H2; unfold Set_rec_table in |- *; rewrite other_site; auto. case (eq_site_dec s0 s); intro. rewrite e1; apply D_post_dec. apply D_post_elsewhere; auto. apply H1; generalize H2; unfold Reset_rec_table in |- *; rewrite other_site; auto. Qed.
imports: DistributedReferenceCounting.machine1.alternate DistributedReferenceCounting.machine1.invariant0 DistributedReferenceCounting.machine1.invariant1 DistributedReferenceCounting.machine1.invariant2 DistributedReferenceCounting.machine1.invariant3 DistributedReferenceCounting.machine1.invariant4