proposition: Lemma alt_post_inc_old : 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_inc_dec. apply alt_null. simpl in |- *. auto. replace m with dec. apply alt_inc_dec. apply alt_any_alt. intro; discriminate. auto. simpl in |- *. case (eq_bool_dec false); intro. discriminate. auto. elim H3; intro. discriminate. inversion H4. auto. elim H3; intro. discriminate. discriminate. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm