proposition: Lemma count_inc_and_dec_D_queue : forall q : queue Message, alternate q -> D_queue q -> (reduce Message dec_count q >= reduce Message new_inc_count q)%Z.
proof: Proof. intros q H. elim H; intros. simpl in |- *; omega. absurd (D_queue (input Message (inc_dec s0) (empty Message))). apply not_D_queue. discriminate. auto. generalize H3. case m. intro; simpl in |- *. generalize (count_inc_and_dec_alt_queue qm H1); intro; omega. intros. absurd (D_queue (input Message (inc_dec s) qm)). apply not_D_queue. discriminate. auto. intros. absurd (D_queue (input Message copy qm)). apply not_D_queue. discriminate. auto. absurd (D_queue (input Message (inc_dec s0) (input Message dec qm))). apply not_D_queue. discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine2.alternate DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4