proposition: Lemma sigma_rooted_fun14 : forall (s1 s2 : Site) (l : list Site), s2 <> owner -> s1 <> owner -> only_once Site eq_site_dec s1 l -> sigma_but Site owner eq_site_dec l (fun s : Site => rooted_fun s s1 s2 copy) = 1%Z.
proof: Proof. intro; intro; intro; intro; intro. elim l. simpl in |- *. intuition. simpl in |- *. intros. case (eq_site_dec a owner). intro. rewrite H1. auto. generalize H2. case (eq_site_dec s1 a). intro. elim H0. rewrite e0; rewrite e. auto. auto. intro. case (eq_site_dec s1 a). intro. generalize (sigma_rooted_fun13 s1 s2 l0 H H0). simpl in |- *. intros. rewrite H3. auto. generalize H2. case (eq_site_dec s1 a). auto. intro. elim n0; auto. intro. rewrite H1. auto. generalize H2. case (eq_site_dec s1 a). intro; elim n0; auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2