proposition: Lemma pos_root_xi : (xi c0 (root_parent s0) > 0)%Z.
proof: Proof. unfold xi in |- *; rewrite rt_root; unfold Int in |- *. generalize (ctrl_copy_pos (bm c0) owner (root_parent s0)). generalize (ctrl_dec_pos (bm c0) owner (root_parent s0)). omega. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc