proposition: Lemma count_alt_queue : forall q : queue Message, alternate q -> (reduce Message dec_count q + 1 >= reduce Message new_inc_count q)%Z /\ (D_queue q -> (reduce Message dec_count q >= reduce Message new_inc_count q)%Z).
proof: Proof. intros. elim H. simpl in |- *. split. omega. intro; omega. intros. simpl in |- *. split. cut (dec_count m >= 0)%Z. intro. cut (new_inc_count m = 0%Z). intro. omega. unfold new_inc_count in |- *. generalize H0. case m; intros. auto. elim (H4 s); auto. auto. elim m; simpl in |- *; intros; omega. intro. decompose [and] H2. generalize H0 H3. case m; simpl in |- *; intros. omega. elim (H6 s). auto. simpl in |- *. cut (D_queue qm). intro. generalize (H5 H8); intro. omega. apply D_input. auto. simpl in |- *; intros. split. decompose [and] H1. cut (D_queue qm). intro. generalize (H4 H5); omega. apply D_dec. auto. auto. intro. inversion H3. generalize H5; simpl in |- *. case (eq_bool_dec true); intro. intro; contradiction. discriminate. Qed.
imports: DistributedReferenceCounting.machine4.alternate DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4