proposition: Lemma pred_dec_send_table : forall (t0 : Send_table) (s0 : Site), Dec_send_table t0 s0 s0 = (t0 s0 - 1)%Z.
proof: Proof. intros; unfold Dec_send_table in |- *; apply that_site. Qed.
imports: DistributedReferenceCounting.machine0.machine