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