proposition: Theorem PRFE_IND_CPA : PRF _ _ _ Rnd Rnd f _ _ (admissible_oc cost) -> IND_CPA_SecretKey (fun n => pair_EqDec (Bvector_EqDec n) (Bvector_EqDec n)) PRFE_KeyGen (fun n => PRFE_Encrypt (@f n)) (admissible_oc cost) (admissible_oc_func_2 cost).
proof: Proof. unfold IND_CPA_SecretKey. intuition. destruct H1. destruct H2. intuition. unfold polynomial_queries_oc, polynomial_queries_oc_func_2 in *. destruct H7. destruct H8. intuition. eapply negligible_le. intuition. eapply PRFE_IND_CPA_concrete. eauto. eauto. eauto. eauto. eauto. eapply negligible_plus. eapply H0. apply PRF_A'_admissible; eauto. unfold admissible_oc; intuition. econstructor; eauto. unfold admissible_oc_func_2; intuition. econstructor; eauto. eapply negligible_plus. eapply negligible_poly_num; intuition. eapply negligible_poly_num; intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime Asymptotic