proposition: Lemma sigma_table2_change : only_once Site eq_site_dec s0 LS1 -> only_once Site eq_site_dec s1 LS2 -> sigma2_table Site LS1 LS2 Data f (update2_table Site eq_site_dec Data t s0 s1 d0) = (sigma2_table Site LS1 LS2 Data f t - f s0 s1 (t s0 s1) + f s0 s1 d0)%Z.
proof: Proof. clear f1 f2. intros H H0. generalize H. unfold sigma2_table in |- *. unfold sigma_table at 1 3 in |- *. elim LS1. simpl in |- *; intuition. simpl in |- *. intros a l H1 H2. case (eq_site_dec s0 a). intro e. rewrite e. unfold update2_table at 1 in |- *. unfold change_x0y0 in |- *. unfold change_x0 at 1 in |- *. rewrite case_eq. apply add_reduce2. generalize (sigma_table_change Site eq_site_dec LS2 Data (t a) s1 d0 (f a)). unfold update_table at 1 in |- *. simpl in |- *. intro H3. rewrite H3. replace (sigma Site l (fun s : Site => Z_id Site s (sigma_table Site LS2 Data (f s) (update2_table Site eq_site_dec Data t a s1 d0 s)))) with (sigma Site l (fun s : Site => sigma_table Site LS2 Data (f s) (t s))). unfold Z_id in |- *. omega. apply sigma_simpl. intros x H4. unfold Z_id in |- *. apply sigma_table_simpl. unfold update2_table in |- *. unfold change_x0y0 in |- *; simpl in |- *. rewrite elsewhere. auto. generalize H2. unfold only_once in |- *. case (eq_site_dec s0 a). rewrite e. intro e0. generalize H4. exact (equality_from_membership Site eq_site_dec a x l). intuition. auto. intro n. rewrite H1. unfold Z_id in |- *. replace (sigma_table Site LS2 Data (f a) (update2_table Site eq_site_dec Data t s0 s1 d0 a)) with (sigma_table Site LS2 Data (f a) (t a)). omega. apply sigma_table_simpl. unfold update2_table in |- *. unfold change_x0y0 in |- *; simpl in |- *. rewrite elsewhere. auto. auto. generalize H2. simpl in |- *. case (eq_site_dec s0 a). intuition. auto. Qed.
imports: List fifo table reduce