proposition: Remark aux5 : forall c : Config, legal c -> sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => reduce Message (fun a : Message => (cardinal_count a - sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))%Z) q) (bm 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) (bm c) + sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => if eq_site_dec s1 owner then reduce Message copy_count q else 0) (bm c) - sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c))%Z.
proof: Proof. intros. rewrite <- sigma2_disjoint. rewrite <- sigma2_disjoint2. apply sigma2_table_simpl_partial. unfold fun_minus_site2 in |- *. unfold fun_minus_site in |- *. unfold fun_sum_site2 in |- *. unfold fun_sum_site in |- *. intros. generalize (not_owner_inc4 c s1 s2 H). generalize (inc_dec_owner4 c s1 s2 H). generalize (inc_dec_owner2 c s1 s2 H). generalize (empty_queue2 c H s1 s2 owner). rewrite H0. clear H0. elim d. intros; simpl in |- *. case (eq_site_dec s2 owner). case (eq_site_dec s1 owner). intros; omega. intros; omega. case (eq_site_dec s1 owner). intros; omega. intros; omega. intros. simpl in |- *. rewrite H0. case (eq_site_dec s2 owner). intro. case (eq_site_dec s1 owner). intro. generalize (H1 e0 e). intro. discriminate. intro. rewrite e. unfold cardinal_count in |- *. unfold fun_sum in |- *. generalize (H4 d0). elim d0. intros. rewrite sigma_rooted_fun3. simpl in |- *. omega. intros. rewrite sigma_rooted_fun5. simpl in |- *. omega. apply finite_site. apply H5. auto. simpl in |- *. left; auto. intros. rewrite sigma_rooted_fun7. simpl in |- *. omega. apply finite_site. auto. intros. case (eq_site_dec s1 owner). intro. rewrite e. simpl in |- *. replace (cardinal_count d0 - sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 d0))%Z with (copy_count d0 - new_inc_count d0)%Z. omega. unfold cardinal_count in |- *. unfold fun_sum in |- *. generalize H3. elim d0. intros. rewrite sigma_rooted_fun9. simpl in |- *. auto. apply finite_site. auto. intros. generalize (H5 e s). simpl in |- *. intro. elim H6. left; auto. rewrite sigma_rooted_fun10. simpl in |- *. auto. intro. replace (cardinal_count d0 - sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0))%Z with (- new_inc_count d0)%Z. omega. simpl in |- *. generalize (H2 n0 n). elim d0. intros. rewrite sigma_rooted_fun12. simpl in |- *. auto. auto. auto. apply finite_site. intros. generalize (H5 s). simpl in |- *. intro. elim H6. left; auto. intros. rewrite sigma_rooted_fun14. simpl in |- *. auto. auto. auto. apply finite_site. intros. generalize (H1 H5 H6). intro; discriminate. intros. generalize (H2 H5 H6 s0). simpl in |- *. intuition. intros. generalize (H3 H5 s0). simpl in |- *. intuition. intros. generalize (H4 m s0 H5). simpl in |- *. intro. apply H7. right; auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3