proposition: Lemma sigma_rooted_fun1 : forall (s s1 s2 : Site) (d : Message), s2 <> owner -> ~ In s1 LS -> ~ In s2 LS -> sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d) = 0%Z.
proof: Proof. intros s s1 s2 d H. elim LS. simpl in |- *. auto. intros. simpl in |- *. case (eq_site_dec a owner). intro. apply H0. generalize H1; simpl in |- *. intuition. generalize H2; simpl in |- *; intuition. intro. rewrite H0. case (eq_site_dec s1 a). generalize H1; simpl in |- *. intro. intro. elim H3. left; auto. intro. case (eq_site_dec s2 a). generalize H2; simpl in |- *; intro; intro. elim H3. left; auto. intro. rewrite sigma_rooted_fun2. omega. auto. auto. auto. generalize H1; simpl in |- *; intuition. generalize H2; simpl in |- *; intuition. Qed.
imports: List DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2