proposition: Lemma invariant1_init : sigma_send_table send_init = (sigma_receive_table rec_init + sigma_weight bag_init - 1)%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. rewrite (sigma_sigma_but Site owner eq_site_dec). case (eq_site_dec owner owner); intro. unfold Int in |- *. rewrite sigma_but_null. omega. intros. case (eq_site_dec s owner). intro; elim H; auto. auto. elim n; auto. apply finite_site. unfold sigma2_table in |- *. unfold sigma_table in |- *. symmetry in |- *. simpl in |- *. rewrite sigma_null. apply sigma_null. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm