proposition: Lemma D_dec_inc : forall q0 : queue Message, alternate q0 -> D_queue q0 -> (card_mess dec q0 >= sigma Site LS (fun s' : Site => card_mess (inc_dec s') q0))%Z.
proof: Proof. intros q0 H; elim H; intros. simpl in |- *; rewrite sigma_null; omega. absurd (D_queue (input Message (inc_dec s0) (empty Message))). apply not_D_queue. trivial. rewrite S_card_mess. rewrite diff_sigma_card_inc. apply alt_dec_inc; trivial. absurd (D_queue (input Message (inc_dec s0) (input Message dec qm))). apply not_D_queue. trivial. Qed.
imports: DistributedReferenceCounting.machine0.machine