proposition: Lemma invariant2 : forall (c0 : Config) (s0 : Site), legal c0 -> s0 <> owner -> st c0 s0 = sigma_rooted s0 (bm c0).
proof: Proof. intros. elim H. apply invariant2_init. intros. apply invariant2_ind. auto. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm