proposition: Lemma alt_dec_inc : forall q0 : queue Message, alternate q0 -> (card_mess dec q0 + 1 >= sigma Site LS (fun s' : Site => card_mess (inc_dec s') q0))%Z.
proof: Proof. intros; elim H; intros. simpl in |- *; rewrite sigma_null; omega. rewrite card_mess_diff. rewrite S_sigma_card_inc. simpl in |- *; rewrite sigma_null; omega. discriminate. rewrite S_card_mess. rewrite diff_sigma_card_inc. omega. rewrite card_mess_diff. rewrite S_card_mess. rewrite S_sigma_card_inc. rewrite diff_sigma_card_inc. omega. discriminate. Qed.
imports: DistributedReferenceCounting.machine0.machine