proposition: Lemma invariant2_init : forall s0 : Site, st config_init s0 = sigma_rooted s0 (bm config_init).
proof: Proof. intros. simpl in |- *. unfold send_init, sigma_rooted, bag_init in |- *. unfold sigma2_table in |- *. unfold sigma_table in |- *. unfold Z_id in |- *. unfold rooted in |- *. simpl in |- *. rewrite sigma_null. rewrite sigma_null. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm