proposition: Theorem A_randomFunc_F_spec : forall x, comp_spec (fun y1 y2 => funcCollision (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split (snd y1))) = funcCollision (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split (snd y2))) /\ (funcCollision (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split (snd y1))) = false -> y1 = y2)) (A (list (list (Bvector b) * Bvector b * Bvector c)) (list_EqDec (pair_EqDec (pair_EqDec (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b)) (Bvector_EqDec c))) (F_randomFunc x) nil) (A (list (list (Bvector b) * Bvector b * Bvector c)) (list_EqDec (pair_EqDec (pair_EqDec (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b)) (Bvector_EqDec c))) (fun (s : list (list (Bvector b) * Bvector b * Bvector c)) (a : list (Bvector b)) => randomFunc_mem (pair_EqDec (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b)) (Bvector_EqDec c) ({ 0 , 1 }^c) s (a, F x a)) nil).
proof: Proof. intuition. eapply comp_spec_consequence. eapply (@oc_comp_spec_eq_until_bad _ _ _ _ _ _ _ _ _ _ _ _ _ (fun z => funcCollision _ _ (fst (split z))) (fun z => funcCollision _ _ (fst (split z))) (fun a b => a = b)). intuition. eapply F_randomFunc_wf. intuition. eapply randomFunc_mem_wf. wftac. intuition; subst. unfold F_randomFunc. unfold randomFunc_mem. case_eq ( arrayLookup (pair_EqDec (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b)) x2 (a, F x a)); intuition. case_eq (arrayLookup_f (Bvector_EqDec b) x2 (F x a)); intuition. eapply comp_spec_ret; intuition. simpl in *. remember (split x2) as z. destruct z. simpl in *. trivial. simpl in *. remember (split x2) as z. destruct z. simpl in *. erewrite arrayLookup_noCollision_eq in H2; eauto. inversion H2; clear H2; subst. trivial. erewrite arrayLookup_noCollision_eq in H2; eauto. inversion H2; clear H2; subst. trivial. eapply funcCollision_false_impl_collidesWith_false. unfold funcCollision in *. simpl in *. destruct (findCollision_1 (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) l a (F x a)). discriminate. assert (l = fst (split x2)). rewrite <- Heqz. trivial. subst. eauto. eapply arrayLookup_Some_In_split. eauto. assert (l = (fst (split x2))). rewrite <- Heqz. trivial. subst. unfold funcCollision in *. simpl in *. unfold collidesWith. destruct (findCollision_1 (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split x2)) a (F x a)). discriminate. trivial. simpl in *. remember (split x2) as z. destruct z. simpl in *. erewrite arrayLookup_noCollision_eq in H2; eauto. inversion H2; clear H2; subst. intuition. unfold funcCollision, collidesWith in *. simpl in *. assert (l = fst (split x2)). rewrite <- Heqz. trivial. subst. destruct (findCollision_1 (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split x2)) a (F x a)). discriminate. trivial. comp_irr_l. eapply comp_spec_ret; intuition. simpl in *. remember (split x2) as z. destruct z. simpl. trivial. simpl in *. remember (split x2) as z. destruct z. simpl in *. erewrite arrayLookup_noCollision_eq in H2; eauto. discriminate. assert (l = fst (split x2)). rewrite <- Heqz. trivial. subst. eapply funcCollision_false_impl_collidesWith_false. unfold funcCollision in *. simpl in *. destruct ( findCollision_1 (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split x2)) a (F x a)). discriminate. eauto. eapply arrayLookup_Some_In_split. eauto. simpl in *. remember (split x2) as z. destruct z. simpl in *. erewrite arrayLookup_noCollision_eq in H2; eauto. discriminate. assert (l = fst (split x2)). rewrite <- Heqz. trivial. subst. eapply funcCollision_false_impl_collidesWith_false. unfold funcCollision in *. simpl in *. destruct ( findCollision_1 (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split x2)) a (F x a)). discriminate. eauto. eapply arrayLookup_Some_In_split. eauto. case_eq (arrayLookup_f (Bvector_EqDec b) x2 (F x a)); intuition. comp_irr_r. eapply comp_spec_ret; intuition. simpl. remember (split x2) as z. destruct z. simpl. trivial. simpl in *. remember (split x2) as z. destruct z. simpl in *. erewrite arrayLookup_noCollision_eq_f in H; eauto. discriminate. unfold funcCollision, collidesWith in *. simpl in *. assert (l = (fst (split x2))). rewrite <- Heqz. trivial. subst. destruct (findCollision_1 (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split x2)) a (F x a)). discriminate. trivial. simpl in *. remember (split x2) as z. destruct z. simpl in *. erewrite arrayLookup_noCollision_eq_f in H; eauto. discriminate. unfold funcCollision, collidesWith in *. simpl in *. assert (l = (fst (split x2))). rewrite <- Heqz. trivial. subst. destruct (findCollision_1 (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split x2)) a (F x a)). discriminate. trivial. comp_skip. apply (oneVector c). apply (oneVector c). eapply comp_spec_ret; intuition. intros. eapply F_randomFunc_preserves_coll; eauto. intuition. eapply randomFunc_mem_preserves_coll; eauto. trivial. trivial. intuition. simpl in *; subst. destruct b1; trivial. Unshelve. trivial. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv