proposition: Lemma invariant4 : forall c : Config, legal c -> st c owner = (sigma_receive_table (rt c) + sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)) + sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)) - sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))%Z.
proof: Proof. intros. rewrite (aux1 c H). rewrite aux2. unfold sigma_weight in |- *. unfold sigma_rooted in |- *. rewrite sigma2_sigma_but. apply add_reduce. rewrite <- sigma2_disjoint2. unfold fun_minus_site2 in |- *. unfold fun_minus_site in |- *. rewrite aux4. rewrite aux5. rewrite simpl_dec_sum. rewrite simpl_copy_sum. rewrite simpl_inc_sum. auto. auto. auto. auto. auto. auto. Qed.
imports: DistributedReferenceCounting.machine1.invariant0 DistributedReferenceCounting.machine1.invariant1 DistributedReferenceCounting.machine1.invariant2 DistributedReferenceCounting.machine1.invariant3