proposition: Lemma in_queue_parent_dec : forall (c1 : Config) (s1 : Site), {s2 : Site | In_queue Message (inc_dec s2) (bm c1 s1 owner)} + {(forall s2 : Site, ~ In_queue Message (inc_dec s2) (bm c1 s1 owner))}.
proof: Proof. intros; elim (bm c1 s1 owner). right; intro; apply not_in_empty. intros; case d; simpl in |- *. elim H; intro y. elim y; intros. left; exists x; auto. right; intro; red in |- *; intros; elim H0; intro. discriminate H1. absurd (In_queue Message (inc_dec s2) q); auto. intros; left; split with s; auto. elim H; intro y. elim y; intros. left; split with x; auto. right; intros; red in |- *; intros; elim H0; intro. discriminate H1. absurd (In_queue Message (inc_dec s2) q); auto. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc