proposition: Lemma sigma2_but_simpl2 : forall (s0 s1 : Site) (t1 t2 : Table2) (f : Site -> Site -> Data -> Z), (forall x y : Site, ~ (x = s0 /\ y = s1) -> f x y (t1 x y) = f x y (t2 x y)) -> only_once Site eq_site_dec s0 LS1 -> only_once Site eq_site_dec s1 LS2 -> sigma2_but_table Site eq_site_dec LS1 LS2 Data s0 s1 f t1 = sigma2_but_table Site eq_site_dec LS1 LS2 Data s0 s1 f t2.
proof: Proof. intros s0 s1 t1 t2 f0 H. elim LS1. simpl in |- *. intros; contradiction. simpl in |- *. intros a l. case (eq_site_dec s0 a); intro. rewrite e. simpl in |- *. intros H0 H1 H2. unfold sigma2_but_table in |- *. unfold sigma_table in |- *; simpl in |- *. unfold Z_id in |- *. case (eq_site_dec a a); intro. apply add_reduce3. generalize H2. elim LS2; simpl in |- *. intro; contradiction. intros a0 l0 H3 H4. unfold sigma_but_table in |- *; simpl in |- *. generalize H4. case (eq_site_dec a0 s1); intro. rewrite e1. case (eq_site_dec s1 s1); intros. rewrite <- (sigma_sigma_but_not_in Site s1 eq_site_dec). rewrite <- (sigma_sigma_but_not_in Site s1 eq_site_dec). apply sigma_simpl. intros x H6. apply H. unfold not in |- *; intro. decompose [and] H7. elim H5; rewrite <- H9; auto. auto. exact H5. elim n; auto. case (eq_site_dec s1 a0); intro. elim n; auto. intros H5. apply add_reduce3. apply H. unfold not in |- *; intro. decompose [and] H6. elim n; auto. generalize H3. unfold sigma_but_table in |- *. auto. apply sigma_simpl. intros x H3. case (eq_site_dec x a); intro. elim H1; rewrite <- e1; auto. apply sigma_simpl. intros x0 H4. apply H. unfold not in |- *; intro. decompose [and] H5; elim n; rewrite <- e; auto. elim n; auto. unfold sigma2_but_table in |- *. unfold sigma_table in |- *; simpl in |- *. intros H0 H1 H2. case (eq_site_dec a s0); intro. elim n; auto. rewrite H0. apply add_reduce3. unfold Z_id in |- *. apply sigma_simpl. intros x H3. apply H. unfold not in |- *; intro; elim n0. decompose [and] H4; auto. auto. auto. auto. Qed.
imports: List fifo table reduce