proposition: Lemma no_inc_dec : forall q : queue Message, (forall s0 : Site, ~ In_queue Message (inc_dec s0) q) -> reduce Message new_inc_count q = 0%Z.
proof: Proof. simple induction q. simpl in |- *. auto. simpl in |- *. intros d q0 H. elim d. simpl in |- *. intro. rewrite H. auto. intro. generalize (H0 s0). intuition. simpl in |- *. intro. intro. generalize (H0 s). intro. elim H1; left; auto. simpl in |- *. intro. rewrite H. auto. intro. generalize (H0 s0). intuition. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3