proposition: Lemma sigma_inc_send_table : forall (t : Send_T) (s : Site), sigma_send_table (Inc_send_table t s) = (sigma_send_table t + 1)%Z.
proof: Proof. intros t s. unfold Inc_send_table in |- *. unfold sigma_send_table in |- *. rewrite (sigma_table_change Site eq_site_dec LS Z t s (t s + 1)%Z (fun (s : Site) (x : Z) => x)). omega. apply finite_site. Qed.
imports: List fifo table reduce sigma2