proposition: Lemma sigma_rooted_fun2 : forall (s s1 s2 : Site) (d : Message), s2 <> owner -> s1 <> s -> s2 <> s -> rooted_fun s s1 s2 d = 0%Z.
proof: Proof. intros. unfold rooted_fun in |- *. elim d. rewrite case_ineq. auto. auto. intro. case (eq_site_dec s0 s). intro; rewrite case_ineq. auto. auto. auto. rewrite case_ineq. auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2