proposition: Lemma invariant1_init : sigma_send_table send_init = (sigma_receive_table rec_init + sigma_weight bag_init)%Z.
proof: Proof. unfold send_init, rec_init, bag_init in |- *. unfold sigma_send_table, sigma_receive_table, sigma_weight in |- *. unfold sigma_table in |- *. simpl in |- *. rewrite sigma_null. replace (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) with 0%Z. omega. unfold sigma2_table in |- *. unfold sigma_table in |- *. symmetry in |- *. simpl in |- *. rewrite sigma_null. apply sigma_null. Qed.
imports: DistributedReferenceCounting.machine1.machine DistributedReferenceCounting.machine1.cardinal DistributedReferenceCounting.machine1.comm