proposition: Lemma decide_rt : forall s : Site, {rt c0 s = false} + {rt c0 s = true}.
proof: Proof. intros. case (rt c0 s). auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4