proposition: Lemma sigma_sigma_but_owner : forall t : Table, sigma_table Site LS Data f t = (sigma_table_but_owner t + f owner (t owner))%Z.
proof: Proof. intros t. unfold sigma_table_but_owner in |- *. unfold sigma_table in |- *. rewrite (sigma_sigma_but Site owner eq_site_dec). auto. apply finite_site. Qed.
imports: List fifo table reduce sigma2