proposition: Lemma in_q_before_first_out : forall q : queue Message, In_queue_before Message dec is_inc_dec q -> In_queue_before Message dec is_inc_dec (first_out Message q).
proof: Proof. simple induction q. simpl in |- *. auto. simpl in |- *. intro. case d. case (eq_bool_dec (is_inc_dec dec)). simpl in |- *. intro; discriminate. intro; intro. case q0. simpl in |- *. auto. simpl in |- *. intros. case (eq_bool_dec false). intro; discriminate. auto. intro. case (eq_bool_dec (is_inc_dec (inc_dec s))). intros; contradiction. simpl in |- *; intro. discriminate. simpl in |- *. case (eq_bool_dec false). intro; discriminate. intro; intro. case q0. simpl in |- *. auto. intros. elim H0. intro; discriminate. intro. generalize (H H1). simpl in |- *. intros. case (eq_bool_dec false); intro. discriminate. right; auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm