proposition: Lemma D_shuffle_copy1 : forall q1 q2 : queue Message, D_queue (input Message copy (append Message q1 q2)) -> D_queue (append Message q1 (input Message copy q2)).
proof: Proof. intros q1 q2. elim q1. simpl in |- *. auto. simpl in |- *. intro. case d; intros. apply D_dec. apply alt_any_alt. intro; discriminate. apply alt_shuffle_copy1. inversion H0. inversion H1. inversion H7. apply alt_any_alt. intro; discriminate. auto. simpl in |- *. case (eq_bool_dec false); intro. discriminate. auto. inversion H0. generalize H2. simpl in |- *. case (eq_bool_dec false); intro. discriminate. case (eq_bool_dec true); intro. intro. elim H4; intro. discriminate. contradiction. discriminate. apply D_dec. apply alt_any_alt. intro; discriminate. apply alt_shuffle_copy1. inversion H0. inversion H1. inversion H7. apply alt_any_alt. intro; discriminate. auto. simpl in |- *. case (eq_bool_dec false); intro. discriminate. right. inversion H0. generalize H2. simpl in |- *. case (eq_bool_dec false); intro. discriminate. intro. elim H4; intro. discriminate. elim H5; intro. discriminate. apply in_q_before_append. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm