proposition: Lemma sigma_rooted_fun6 : forall (s s1 : Site) (l : list Site), ~ In s l -> sigma_but Site owner eq_site_dec l (fun s0 : Site => rooted_fun s0 s owner copy) = 0%Z.
proof: Proof. intro; intro; intro. elim l. simpl in |- *. auto. simpl in |- *. intros. case (eq_site_dec a owner). intro. rewrite H. auto. generalize H0; intuition. intro. case (eq_site_dec s a). intro. elim H0. left; auto. intro. rewrite H. auto. generalize H0; intuition. Qed.
imports: List DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2