proposition: Remark S_card_mess : forall (q0 : queue Message) (m : Message), card_mess m (input Message m q0) = (card_mess m q0 + 1)%Z.
proof: Proof. intros; unfold card_mess in |- *; apply input_S_card; trivial. Qed.
imports: DistributedReferenceCounting.machine0.machine