proposition: Lemma st_rt_init : forall s0 : Site, (st config_init s0 > 0)%Z -> rt config_init s0 = true.
proof: Proof. intro; unfold config_init in |- *; simpl in |- *; unfold send_init in |- *; intros. absurd (0 > 0)%Z; omega. Qed.
imports: DistributedReferenceCounting.machine0.machine counting