proposition: Lemma simpl_inc_sum : forall c : Config, legal c -> sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c) = sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)).
proof: Proof. intros. unfold sigma2_table in |- *. generalize (inc_dec_owner2 c). generalize (inc_dec_owner3 c). generalize (bm c). intros. apply sigma_table_simpl. apply funct_eq. intros. unfold sigma_table in |- *. case (eq_site_dec e owner). intro. rewrite (sigma_sigma_but Site owner eq_site_dec (fun s : Site => reduce Message new_inc_count (b e s))) . replace (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) with 0%Z. omega. rewrite sigma_but_null. auto. intros. generalize (H0 e s H H2). intro. apply no_inc_dec. auto. apply finite_site. intro. rewrite (sigma_sigma_but Site owner eq_site_dec (fun s : Site => reduce Message new_inc_count (b e s))) . replace (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) with 0%Z. auto. rewrite sigma_but_null. auto. intros. generalize (H1 e s H n H2). intro. apply no_inc_dec. auto. apply finite_site. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3