proposition: Remark aux1 : forall c : Config, legal c -> st c owner = (sigma_receive_table (rt c) + sigma_weight (bm c) - sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c))%Z.
proof: Proof. intros. unfold sigma_send_table in |- *. generalize (invariant1 c H). unfold sigma_send_table in |- *. rewrite sigma_sigma_but_owner. generalize (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c)). intros. omega. Qed.
imports: DistributedReferenceCounting.machine1.invariant0 DistributedReferenceCounting.machine1.invariant1 DistributedReferenceCounting.machine1.invariant2 DistributedReferenceCounting.machine1.invariant3