proposition: Remark yi_init : (fun s0 : Site => yi config_init s0) = (fun s0 : Site => 0%Z).
proof: Proof. apply funct_eq; intros; unfold yi in |- *; simpl in |- *; apply sigma_null. Qed.
imports: DistributedReferenceCounting.machine0.machine counting