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