proposition: Theorem Rnd_split_equiv : forall n1 n2 z , evalDist (x <-$ {0, 1}^(n1 + n2); ret (splitVector n1 n2 x)) z == evalDist (x1 <-$ {0, 1}^n1; x2 <-$ {0, 1}^n2; ret (x1, x2)) z.
proof: Proof. intuition. eapply det_eq_impl_dist_sem_eq; wftac. unfold evalDet_equiv. intuition. inversion H; clear H; subst. inversion H0; clear H0; subst. simpl in *. case_eq (shiftOut s (plus n1 n2)); intuition. destruct p. specialize (shiftOut_plus _ _ _ H); intuition. destruct H0. destruct H0. destruct H0. intuition. rewrite H in H4. inversion H4; clear H4; subst. simpl in *. inversion H8; clear H8; subst. simpl in *. inversion H7; clear H7; subst. econstructor. econstructor. eauto. simpl. rewrite H1. econstructor. eauto. simpl. econstructor. eauto. simpl. rewrite H0. econstructor. eauto. simpl. econstructor. eauto. rewrite H3. econstructor. rewrite H in H4. inversion H4; clear H4; subst. inversion H0; clear H0; subst. simpl in *. case_eq (shiftOut s (n1 + n2)); intuition. rewrite H in H4. destruct p. inversion H4; clear H4; subst. simpl in *. inversion H5; clear H5; subst. simpl in *. inversion H4. specialize (shiftOut_plus_None _ _ _ H); intuition. econstructor. econstructor. eauto. simpl. rewrite H1. econstructor. destruct H1. destruct H0. intuition. econstructor. econstructor. eauto. simpl. rewrite H1. econstructor. eauto. simpl. econstructor. eauto. simpl. rewrite H2. econstructor. inversion H; clear H; subst. inversion H0; clear H0; subst. simpl in *. case_eq (shiftOut s n1); intuition. rewrite H in H4. destruct p. inversion H4; clear H4; subst. inversion H5; clear H5; subst. simpl in *. case_eq (shiftOut b1 n2); intuition. rewrite H0 in H4. destruct p. inversion H4; clear H4; subst. simpl in *. inversion H6; clear H6; subst. simpl in *. inversion H5; clear H5; subst. econstructor. econstructor. eauto. simpl. erewrite shiftOut_plus_if; eauto. econstructor. eauto. simpl. econstructor. eauto. simpl. rewrite splitVector_append. econstructor. rewrite H0 in H4. inversion H4; clear H4; subst. rewrite H in H4. inversion H4. inversion H0; clear H0; subst. simpl in *. case_eq (shiftOut s n1); intuition. rewrite H in H4. destruct p. inversion H4; clear H4; subst. simpl in *. inversion H5; clear H5; subst. simpl in *. case_eq (shiftOut b1 n2); intuition. rewrite H0 in H4. destruct p. inversion H4; clear H4; subst. simpl in *. inversion H6; clear H6; subst. simpl in *. inversion H5. econstructor. econstructor. eauto. simpl. erewrite shiftOut_plus_None_if. econstructor. right. econstructor. econstructor. intuition. eauto. trivial. rewrite H in H4. econstructor. econstructor. eauto. simpl. erewrite shiftOut_plus_None_if. econstructor. intuition. Qed.
imports: FCF.FCF FCF.SemEquiv FCF.DetSem