proposition: Lemma sigma_weight_change_queue : forall (s1 s2 s3 : Site) (b : Bag_of_message) (q : queue Message), b s1 s2 = input Message dec (input Message (inc_dec s3) q) -> sigma_weight (change_queue (queue Message) b s1 s2 q) = (sigma_weight b - cardinal_count dec - cardinal_count (inc_dec s3))%Z.
proof: Proof. intros. unfold sigma_weight in |- *. rewrite sigma2_sigma2_but_x_y with (s0 := s1) (s1 := s2) (eq_site_dec := eq_site_dec). rewrite sigma2_sigma2_but_x_y with (s0 := s1) (s1 := s2) (eq_site_dec := eq_site_dec). unfold cardinal in |- *. rewrite that_queue. rewrite H. simpl in |- *. apply add_reduce. apply sigma2_but_simpl2. intros. case (eq_queue_dec s1 x s2 y); intro. elim H0. split; decompose [and] a; auto. rewrite other_queue. auto. elim o; auto. apply finite_site. apply finite_site. apply finite_site. apply finite_site. apply finite_site. apply finite_site. Qed.
imports: reduce DistributedReferenceCounting.machine4.cardinal sigma2 sum