proposition: Lemma simpl_copy_sum : forall c : Config, legal c -> sigma2_table Site LS LS (queue Message) (fun (s1 _ : Site) (q : queue Message) => match eq_site_dec s1 owner with | left _ => reduce Message copy_count q | right _ => 0%Z end) (bm c) = sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)).
proof: Proof. intros. unfold sigma2_table in |- *. unfold sigma in |- *. unfold sigma_table in |- *. rewrite (sigma_sigma_but Site owner eq_site_dec (fun s : Site => Z_id Site s (sigma Site LS (fun s0 : Site => match eq_site_dec s owner with | left _ => reduce Message copy_count (bm c s s0) | right _ => 0%Z end)))). rewrite Z_id_reduce. replace (sigma_but Site owner eq_site_dec LS (fun s : Site => Z_id Site s (sigma Site LS (fun s0 : Site => match eq_site_dec s owner with | left _ => reduce Message copy_count (bm c s s0) | right _ => 0%Z end)))) with 0%Z. simpl in |- *. apply sigma_simpl. intros. rewrite case_eq. rewrite Z_id_reduce. auto. rewrite sigma_but_null. auto. intros. rewrite Z_id_reduce. case (eq_site_dec s owner). intro; elim H0; auto. intro. apply sigma_null. apply finite_site. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3