proposition: Lemma invariant5 : forall c : Config, legal c -> forall s : Site, (Int (rt c s) + reduce Message dec_count (bm c s owner) + reduce Message copy_count (bm c owner s) - reduce Message new_inc_count (bm c s owner) >= 0)%Z.
proof: Proof. intros. generalize (copy_count_is_positive (bm c owner s)); intro. generalize (legal_alternate s c H); intro. case (eq_bool_dec (rt c s)); intro; rewrite e; unfold Int in |- *. decompose [and] H1. generalize (count_inc_and_dec_alt_queue (bm c s owner) H2); intro. omega. decompose [and] H1. generalize (H3 e); intro. generalize (count_inc_and_dec_D_queue (bm c s owner) H2 H4); intro. omega. Qed.
imports: DistributedReferenceCounting.machine3.alternate DistributedReferenceCounting.machine3.invariant0 DistributedReferenceCounting.machine3.invariant1 DistributedReferenceCounting.machine3.invariant2 DistributedReferenceCounting.machine3.invariant3 DistributedReferenceCounting.machine3.invariant4