proposition: Remark aux4 : forall t : Site -> Site -> queue Message, sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => (cardinal q - sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 q))%Z) t = sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => reduce Message (fun a : Message => (cardinal_count a - sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))%Z) q) t.
proof: Proof. intros. unfold sigma2_table in |- *. apply sigma_table_simpl. apply funct_eq. intros. apply sigma_table_simpl2. intros. apply aux3. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3