proposition: Lemma not_owner_inc2 : forall (c : Config) (s0 s1 s2 : Site), legal c -> In_queue Message (inc_dec s0) (bm c s1 s2) -> s0 <> owner.
proof: Proof. intros. generalize (not_owner_inc c s1 s2 H). intro. generalize (equality_from_queue_membership Message eq_message_dec (inc_dec owner) (inc_dec s0) (bm c s1 s2)). intros. generalize (H2 H0 H1). intro. case (eq_site_dec s0 owner). intro. rewrite e in H3. generalize H3. intuition. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm