proposition: Lemma sigma2_disjoint : sigma2_table Site LS1 LS2 Data (fun_sum_site2 f1 f2) t = (sigma2_table Site LS1 LS2 Data f1 t + sigma2_table Site LS1 LS2 Data f2 t)%Z.
proof: Proof. unfold sigma2_table in |- *. unfold fun_sum_site2 in |- *. rewrite <- sigma_same_table. apply sigma_table_simpl. unfold fun_sum_site in |- *. apply funct_eq. intro e. unfold fun_sum in |- *. rewrite <- sigma_disjoint. unfold fun_sum_site in |- *. auto. Qed.
imports: List fifo table reduce