proposition: Lemma alt_shuffle_copy2 : forall q1 q2 : queue Message, alternate (append Message q1 (input Message copy q2)) -> alternate (append Message q1 q2).
proof: Proof. intros q1 q2. elim q1. simpl in |- *. auto. intro. inversion H. auto. simpl in |- *. intro. case d; intros. apply alt_any_alt. intro; discriminate. apply H. inversion H0. auto. inversion H0. apply alt_inc_dec. apply H. auto. elim (H3 s); auto. apply alt_inc_dec. apply H. auto. apply in_q_before_append2. auto. apply alt_any_alt. intro; discriminate. inversion H0. apply H. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm