proposition: Remark S_sigma_card_inc : forall (s0 : Site) (q0 : queue Message), sigma Site LS (fun s' : Site => card_mess (inc_dec s') (input Message (inc_dec s0) q0)) = (sigma Site LS (fun s' : Site => card_mess (inc_dec s') q0) + 1)%Z.
proof: Proof. intros; apply sigma__S with (eq_E_dec := eq_site_dec) (x0 := s0). exact finite_site. apply S_card_mess. intros; apply card_mess_diff; injection; auto. Qed.
imports: DistributedReferenceCounting.machine0.machine