proposition: Lemma sigma2_disjoint2 : sigma2_table Site LS1 LS2 Data (fun_minus_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_minus_site2 in |- *. rewrite <- sigma_same_table2. apply sigma_table_simpl. unfold fun_minus_site in |- *. apply funct_eq. intro e. unfold fun_minus in |- *. rewrite <- sigma_disjoint2. unfold fun_minus_site in |- *. auto. Qed.
imports: List fifo table reduce