proposition: Lemma not_owner_inc3 : forall (c : Config) (s1 s2 : Site), legal c -> forall s0 : Site, In_queue Message (inc_dec s0) (bm c s1 s2) -> s0 <> owner.
proof: Proof. intros. apply (not_owner_inc2 c s0 s1 s2). auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm