proposition: Lemma count_inc_and_dec_alt_queue : forall q : queue Message, alternate q -> (reduce Message dec_count q + 1 >= reduce Message new_inc_count q)%Z.
proof: Proof. intros. elim H. simpl in |- *; omega. intro; simpl in |- *; omega. simpl in |- *; intros. generalize H0; case m; simpl in |- *. intro; omega. intros. elim (H3 s); auto. intro; omega. simpl in |- *; intros. omega. Qed.
imports: DistributedReferenceCounting.machine2.alternate DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4