proposition: Lemma copy_count_is_positive : forall q : queue Message, (reduce Message copy_count q >= 0)%Z.
proof: Proof. intros. apply reduce_positive_or_null. intro. elim a; simpl in |- *; intros; omega. Qed.
imports: DistributedReferenceCounting.machine2.alternate DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4