proposition: Theorem PRF_A_randomFunc_eq_until_bad : comp_spec (fun y1 y2 => hasDups _ (fst (split (snd y1))) = hasDups _ (fst (split (snd y2))) /\ (hasDups _ (fst (split (snd y1))) = false -> snd y1 = snd y2 /\ fst y1 = fst y2)) (PRF_A _ _ randomFunc_withDups nil) (PRF_A _ _ (fun (ls : list (D * Bvector eta)) (x : D) => r <-$ { 0 , 1 }^eta; ret (r, (x, r) :: ls)) nil).
proof: Proof. eapply (fcf_oracle_eq_until_bad (fun x => hasDups _ (fst (split x))) (fun x => hasDups _ (fst (split x))) eq); intuition. apply PRF_A_wf. unfold randomFunc_withDups. destruct ( arrayLookup D_EqDec a b); fcf_well_formed. fcf_well_formed. subst. unfold randomFunc_withDups. case_eq (arrayLookup _ x2 a); intuition. fcf_irr_r. fcf_simp. fcf_spec_ret; simpl. remember (split x2) as z. destruct z. simpl in *. trivial. simpl in *. remember (split x2) as z. destruct z. simpl in *. destruct (in_dec (EqDec_dec D_EqDec) a l0); intuition. discriminate. rewrite notInArrayLookupNone_unzip in H. discriminate. intuition. rewrite unzip_eq_split in H3. remember (split x2) as z. destruct z. pairInv. simpl in *. intuition. simpl in *. remember (split x2) as z. destruct z. simpl in *. destruct (in_dec (EqDec_dec D_EqDec) a l0). discriminate. rewrite notInArrayLookupNone_unzip in H. discriminate. intuition. rewrite unzip_eq_split in H3. remember (split x2) as z. destruct z. pairInv. simpl in *. intuition. fcf_skip. fcf_spec_ret. unfold randomFunc_withDups in *. fcf_simp_in_support. simpl. remember (split c0) as z. destruct z. simpl in *. destruct (in_dec (EqDec_dec D_EqDec) d l0); intuition. fcf_simp_in_support. simpl in *. remember (split c0) as z. destruct z. simpl in *. destruct (in_dec (EqDec_dec D_EqDec) d l0); intuition. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF