proposition: Lemma sigma2_sigma2_but_x_y : forall (s0 s1 : Site) (t : Table2), only_once Site eq_site_dec s0 LS1 -> only_once Site eq_site_dec s1 LS2 -> sigma2_table Site LS1 LS2 Data f t = (sigma2_but_table Site eq_site_dec LS1 LS2 Data s0 s1 f t + f s0 s1 (t s0 s1))%Z.
proof: Proof. intro s0. intro s1. intro t. elim LS1. simpl in |- *. intros; contradiction. intros a l H H0 H1. unfold sigma2_table, sigma2_but_table in |- *. simpl in |- *. case (eq_site_dec a s0); intro. unfold sigma_table in |- *. rewrite (sigma_sigma_but Site a eq_site_dec). rewrite (sigma_sigma_but Site a eq_site_dec) with (l := a :: l). simpl in |- *. case (eq_site_dec a a). intro e0. case (eq_site_dec a s0). intro e1. rewrite <- sigma_sigma_but_not_in with (x0 := a). rewrite <- sigma_sigma_but_not_in with (x0 := a). rewrite (sigma_sigma_but Site s1 eq_site_dec) with (l := LS2). unfold sigma_but_table in |- *. rewrite e1. unfold Z_id in |- *. apply add_reduce2_1. apply sigma_simpl. intros x H2. case (eq_site_dec x s0). intro e2. generalize H0; rewrite e1. simpl in |- *. case (eq_site_dec s0 s0); intro. intro H3. elim H3; rewrite <- e2; auto. elim n; auto. intro n. auto. auto. generalize H0; simpl in |- *. rewrite e. case (eq_site_dec s0 s0); intro. auto. elim n; auto. generalize H0; simpl in |- *. case (eq_site_dec s0 a); intro. rewrite e; auto. elim n; auto. intro n. elim n; auto. intro n. elim n; auto. rewrite e; auto. generalize H0; rewrite e; auto. generalize H0; rewrite e. auto. unfold sigma_table in |- *; simpl in |- *. generalize H. unfold sigma2_table in |- *. unfold sigma_table in |- *. intro H2. rewrite H2. unfold Z_id in |- *; simpl in |- *. case (eq_site_dec a s0); intro. elim n; auto. unfold sigma2_but_table in |- *. unfold sigma_table in |- *. unfold Z_id in |- *. omega. generalize H0; simpl in |- *. case (eq_site_dec s0 a); intro. elim n; auto. auto. auto. Qed.
imports: List fifo table reduce