proposition: Lemma simpl_dec_sum : forall c : Config, legal c -> sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => if eq_site_dec s2 owner then reduce Message dec_count q else 0%Z) (bm c) = sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)).
proof: Proof. intros. unfold sigma2_table in |- *. apply sigma_table_simpl. apply funct_eq. intros. unfold sigma_table in |- *. rewrite (sigma_sigma_but Site owner eq_site_dec (fun s : Site => match eq_site_dec s owner with | left _ => reduce Message dec_count (bm c e s) | right _ => 0%Z end)). replace (sigma_but Site owner eq_site_dec LS (fun s : Site => match eq_site_dec s owner with | left _ => reduce Message dec_count (bm c e s) | right _ => 0%Z end)) with 0%Z. case (eq_site_dec owner owner). intro; auto. intuition. rewrite sigma_but_null. auto. intros. rewrite case_ineq. auto. auto. apply finite_site. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3