proposition: Lemma alt_post_inc : forall s1 : Site, alternate (b0 s0 owner) -> b0 s0 owner = empty Message \/ last Message (b0 s0 owner) = value Message dec -> alternate (Post_message Message (inc_dec s1) b0 s0 owner s0 owner).
proof: Proof. intros s1 H; rewrite post_here; inversion H; simpl in |- *; intros. apply alt_single_inc. decompose [or] H0; discriminate H2. elim H3. intro. discriminate. intro. replace m with dec. apply alt_inc_dec. auto. inversion H4. auto. decompose [or] H2; discriminate H3. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm