proposition: Lemma inc_dec_in_collect2 : forall (b : Bag_of_message) (m : Message) (s0 s1 s2 s3 : Site), first Message (b s1 s2) = value Message m -> inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) -> inc_dec_in_queue s3 (b s0 owner).
proof: Proof. intros b m s0 s1 s2 s3 H. case (eq_queue_dec s1 s0 s2 owner). intros. decompose [and] a. generalize H0. rewrite H1; rewrite H2. rewrite collect_here. elim (b s0 owner). simpl in |- *. auto. intros d q. case q. simpl in |- *. intuition. intro. case d. simpl in |- *. auto. intro. case (eq_site_dec s s3). intro. rewrite e. simpl in |- *. auto. case (eq_site_dec s3 s3). auto. intro. elim n. auto. intro. simpl in |- *. auto. auto. simpl in |- *. auto. intro. rewrite collect_elsewhere. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4