proposition: Lemma inc_dec_owner : forall (c : Config) (s1 s2 : Site), legal c -> s1 = owner \/ s2 <> owner -> forall s0 : Site, ~ In_queue Message (inc_dec s0) (bm c s1 s2).
proof: Proof. intros c s1 s2 H. elim H. simpl in |- *. intros; unfold not in |- *; auto. simple induction t; simpl in |- *; intros. apply not_in_queue_post. discriminate. auto. apply not_in_queue_collect. auto. apply not_in_queue_post. discriminate. apply not_in_queue_collect; auto. apply not_in_queue_post. discriminate. apply not_in_queue_collect. auto. apply not_in_queue_collect. auto. case (eq_queue_dec s3 s1 owner s2). intro; decompose [and] a. elim H2. intro. cut (s3 <> owner). intro. elim H6. rewrite H3; rewrite H5; auto. unfold not in |- *; intro. generalize (no_copy_to_owner c0 H0 s0). intro. elim H7; rewrite <- H6; auto. apply first_in. auto. intro. elim H3; auto. intro; rewrite post_elsewhere. apply not_in_queue_collect. auto. auto. apply not_in_queue_post. discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine1.machine DistributedReferenceCounting.machine1.cardinal DistributedReferenceCounting.machine1.comm