proposition: Lemma sigma_reduce_pos : forall (s0 s1 : Site) (bom : Bag_of_message), (forall m : Data, (f m > 0)%Z) -> (sigma_reduce bom >= 0)%Z.
proof: Proof. intros s1 s2 bom H. unfold sigma_reduce in |- *. apply sigma_pos. intro x_. apply reduce_positive. auto. Qed.
imports: reduce table abstract_machine