proposition: Lemma alt_shuffle_copy : forall q1 q2 q3 q4 : queue Message, append Message q1 q2 = append Message q3 q4 -> alternate (append Message q1 (input Message copy q2)) -> alternate (append Message q3 (input Message copy q4)).
proof: Proof. intros. apply alt_shuffle_copy1. rewrite <- H. apply alt_any_alt. intro; discriminate. generalize H0. elim q1; simpl in |- *. intro. inversion H1; auto. intro. case d; intros. apply alt_any_alt. intro; discriminate. apply H1. inversion H2; auto. inversion H2. elim (H5 s); auto. apply alt_inc_dec. apply H1. auto. apply in_q_before_append2. auto. apply alt_any_alt. intro; discriminate. apply H1. inversion H2. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm