proposition: Lemma disjoint_cardinal : forall q : queue Message, cardinal q = (reduce Message dec_count q + (reduce Message inc_count q + reduce Message copy_count q))%Z.
proof: Proof. intro. rewrite <- disjoint_reduce. rewrite <- disjoint_reduce. unfold cardinal in |- *. unfold cardinal_count in |- *. auto. Qed.
imports: reduce DistributedReferenceCounting.machine2.machine