proposition: Lemma sigma_table_change : only_once Site eq_site_dec s0 LS -> sigma_table Site LS Data f (update_table Site eq_site_dec Data t s0 d0) = (sigma_table Site LS Data f t - f s0 (t s0) + f s0 d0)%Z.
proof: Proof. unfold sigma_table in |- *. unfold update_table in |- *. elim LS. simpl in |- *. intuition. intros a l H. case (eq_site_dec s0 a). intro; rewrite e. simpl in |- *. unfold change_x0 in |- *. case (eq_site_dec a a). intros e0 H0. replace (sigma Site l (fun s : Site => f s match eq_site_dec a s with | left _ => d0 | right _ => t s end)) with (sigma Site l (fun s : Site => f s (t s))). omega. apply sigma_simpl. intros x H1. case (eq_site_dec a x). intro; rewrite e1 in H0. intuition. intro; auto. intro n. elim n. auto. intro n. intro H0. simpl in |- *. rewrite H. unfold change_x0 in |- *. rewrite case_ineq. omega. auto. unfold only_once in H0. generalize H0. case (eq_site_dec s0 a). intuition. unfold only_once in |- *. auto. Qed.
imports: List fifo table reduce