proposition: Lemma in_q_before_append : forall q1 q2 : queue Message, In_queue_before Message dec is_inc_dec (append Message q1 q2) -> In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)).
proof: Proof. simple induction q1; simpl in |- *. case (eq_bool_dec false); intro. discriminate. intros. right; auto. intro. case d. simpl in |- *. case (eq_bool_dec false); intro. discriminate. intros. auto. intro. simpl in |- *. case (eq_bool_dec true). auto. intro; discriminate. simpl in |- *. case (eq_bool_dec false); intro. discriminate. intros. right. apply H. elim H0; intro. discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm