proposition: Lemma D_shuffle_copy : forall q1 q2 q3 q4 : queue Message, append Message q1 q2 = append Message q3 q4 -> D_queue (append Message q1 (input Message copy q2)) -> D_queue (append Message q3 (input Message copy q4)).
proof: Proof. intros. apply D_shuffle_copy1. apply D_dec. inversion H0. generalize H2. case q1; simpl in |- *. intro; discriminate. intros; discriminate. apply alt_any_alt. intro; discriminate. apply alt_shuffle_copy2. apply alt_shuffle_copy with (q1 := q1) (q2 := q2). auto. auto. inversion H0. generalize H2. case q1; simpl in |- *; intros; discriminate. rewrite <- H. simpl in |- *. case (eq_bool_dec false); intro. discriminate. right. apply in_q_before_append2. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm