proposition: Lemma sigma_rooted_fun5 : forall s s1 : Site, only_once Site eq_site_dec s LS -> s <> owner -> sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted_fun s0 s1 owner (inc_dec s)) = 1%Z.
proof: Proof. intro; intro. elim LS. simpl in |- *. intuition. intros. case (eq_site_dec a owner). intro. generalize H0. case (eq_site_dec s a). rewrite e. intuition. generalize H. simpl in |- *. intros. rewrite H2. case (eq_site_dec a owner). auto. intuition. generalize H3. case (eq_site_dec s a). intuition. auto. auto. intros. generalize H. generalize (sigma_rooted_fun4 s s1 l). simpl in |- *. intros. rewrite case_ineq. case (eq_site_dec s a). intro. rewrite H2. rewrite case_eq. auto. generalize H0; simpl in |- *. case (eq_site_dec s a). auto. intuition. intros. rewrite H3. auto. generalize H0; simpl in |- *. case (eq_site_dec s a). intuition. auto. auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2