proposition: Lemma rooted_fun_positive_or_null : forall (s0 x y : Site) (a : Message), (rooted_fun s0 x y a >= 0)%Z.
proof: Proof. intros. unfold rooted_fun in |- *. elim a. case (eq_site_dec y s0). intro; omega. intro; omega. intro. case (eq_site_dec s s0). case (eq_site_dec y owner). intros; omega. intros; omega. intros; omega. case (eq_site_dec x s0). intros; omega. intros; omega. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm