proposition: Theorem PRF_A'_poly_time : poly_time_nonuniform_oc cost _ _ _ (fun n => PRF_A' (A1 n) (@A2 n)).
proof: Proof. intuition. unfold PRF_A'. unfold poly_time_nonuniform_oc. destruct (PRFE_Encrypt_OC_poly_time). destruct H0. unfold admissible_oc in *. unfold admissible_oc_func_2 in *. intuition. destruct H0. destruct H2. destruct H2. intuition. exists (fun x o : nat => x1 x (o + 5 * x) + x2 x (o + 5 * x) + o + 5 * (x3 x) + 6 + 7 * x). intuition. eapply polynomial_plus. eapply polynomial_plus. eapply polynomial_plus. eapply polynomial_plus. eapply polynomial_plus. eapply H6. eapply polynomial_plus; intuition. eapply polynomial_mult. eapply polynomial_const. eapply polynomial_ident. eapply H0. eapply polynomial_plus; intuition. eapply polynomial_mult. eapply polynomial_const. eapply polynomial_ident. intuition. eapply polynomial_mult. eapply polynomial_const. intuition. eapply polynomial_const. eapply polynomial_mult. eapply polynomial_const. eapply polynomial_ident. eapply oc_cost_le. eapply PRF_A'_cost; eauto. eapply H12. intuition. eapply H12. intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime Asymptotic