proposition: Lemma parent_rt : forall s0 s1 : Site, parent c0 s1 s0 -> rt c0 s1 = true.
proof: Proof. intros; elim H; intros; apply st_rt. apply (not_owner_inc c0 s2 s3 owner); trivial. rewrite two. apply sigma_ctrl_strct_pos with (s1 := s3); trivial. trivial. apply (not_owner_inc c0 s2 s3 owner); auto. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc