proposition: Lemma owner_rt_true : forall c : Config, legal c -> rt c owner = true.
proof: Proof. intros. elim H. simpl in |- *. unfold rec_init in |- *; simpl in |- *. case (eq_site_dec owner owner). auto. intro. elim n. auto. simple induction t; simpl in |- *; intros; auto. unfold Set_rec_table in |- *; rewrite other_site; auto. unfold not in |- *; intro; generalize e. rewrite H2; rewrite H1; auto with bool. unfold Set_rec_table in |- *; rewrite other_site; auto. unfold Reset_rec_table in |- *; rewrite other_site; auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm