proposition: Lemma sigma_reset_receive_table : forall (t : Recv_T) (s : Site), t s = true -> sigma_receive_table (Reset_rec_table t s) = (sigma_receive_table t - 1)%Z.
proof: Proof. intros t s H. unfold Reset_rec_table in |- *. unfold sigma_receive_table in |- *. rewrite (sigma_table_change Site eq_site_dec LS bool t s false). rewrite H. simpl in |- *. omega. apply finite_site. Qed.
imports: List fifo table reduce sigma2