proposition: Lemma decide_no_rt : forall c : Config, {no_rt c} + {(exists s1 : Site, s1 <> owner /\ rt c s1 = true)}.
proof: Proof. intros. unfold no_rt in |- *. elim LS. simpl in |- *. left; contradiction. intros. case (eq_site_dec a owner); intro. elim H; intro. left. intros. generalize H0; simpl in |- *. case (eq_site_dec s1 a); intro. elim H1; rewrite e0; auto. intro. elim H2; auto. intro; elim n; auto. right; auto. elim (decide_rt c a); intro. elim H; intro. left; intros. case (eq_site_dec s1 a); intro. rewrite e; auto. apply a1. generalize H0; simpl in |- *; intro. elim H2; intro; auto. elim n0; auto. auto. right; auto. right. split with a. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8