proposition: Theorem PRF_A'_poly_queries : polynomial_queries_oc _ _ _ (fun n => PRF_A' (A1 n) (@A2 n)).
proof: Proof. unfold admissible_oc, admissible_oc_func_2 in *. intuition. destruct H5. destruct H6. intuition. exists (fun n => x n + (1 + x0 n)). intuition. eapply polynomial_plus; intuition. eapply polynomial_plus; intuition. eapply polynomial_const. eapply qam_le. econstructor. econstructor. eauto. intuition. eapply PRFE_Encrypt_OC_qam. intuition. econstructor. econstructor. econstructor. intuition. econstructor. econstructor. intuition. econstructor. econstructor. intuition. econstructor. econstructor. econstructor. eapply H8. eapply Nat.le_refl. eapply Nat.le_refl. intuition. eapply PRFE_Encrypt_OC_qam. intuition. econstructor. lia. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime Asymptotic