proposition: Lemma other_definition_for_sigma_receive_table : forall t : Recv_T, sigma_receive_table t = sigma_table Site LS Z (Z_id Site) (fun s : Site => Int (t s)).
proof: Proof. intros. unfold sigma_receive_table in |- *. unfold sigma_table in |- *. unfold Z_id in |- *. auto. Qed.
imports: DistributedReferenceCounting.machine2.alternate DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4