proposition: Remark aux2 : forall c : Config, legal c -> sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c) = sigma_but Site owner eq_site_dec LS (fun s : Site => sigma_rooted s (bm c)).
proof: Proof. intros. unfold sigma_table_but_owner in |- *. apply sigma_but_simpl. intros. rewrite (invariant2 c s). auto. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3