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