proposition: Lemma invariant1 : forall c : Config, legal c -> sigma_send_table (st c) = (sigma_receive_table (rt c) + sigma_weight (bm c) - 1)%Z.
proof: Proof. intros. elim H. apply invariant1_init. exact invariant1_inductive. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm