proposition: Lemma sigma_rooted_fun9 : forall (s2 : Site) (l : list Site), only_once Site eq_site_dec s2 l -> s2 <> owner -> sigma_but Site owner eq_site_dec l (fun s : Site => rooted_fun s owner s2 dec) = 1%Z.
proof: Proof. simple induction l. simpl in |- *; intuition. intros. generalize H. generalize (sigma_rooted_fun8 s2 l0). simpl in |- *. intros. case (eq_site_dec a owner). intros. apply H3. generalize H0; simpl in |- *. case (eq_site_dec s2 a). rewrite e. intuition. auto. auto. intro. case (eq_site_dec s2 a). auto. intro. rewrite H2. auto. generalize H0. rewrite e; simpl in |- *. case (eq_site_dec a a). auto. intuition. intro. rewrite H3. auto. generalize H0. simpl in |- *. case (eq_site_dec s2 a). intuition. auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2