proposition: Lemma alt_post_inc : forall s1 : Site, alternate (b0 s0 owner) -> In_queue_before Message dec is_inc_dec (b0 s0 owner) -> alternate (Post_message Message (inc_dec s1) b0 s0 owner s0 owner).
proof: Proof. intros s1 H; rewrite post_here. inversion H; intros. apply alt_inc_dec. apply alt_null. auto. generalize H1 H2 H3. case m. intros. apply alt_inc_dec. apply alt_any_alt. intro; discriminate. auto. auto. intros. elim (H4 s); auto. intros. apply alt_inc_dec. apply alt_any_alt. auto. auto. auto. generalize H3. simpl in |- *. case (eq_bool_dec true); intro. intro; contradiction. discriminate. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm