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