proposition: Theorem PRFE_Encrypt_OC_poly_time : poly_time_nonuniform_oc_func_2 cost _ _ _ _ _ PRFE_Encrypt_OC.
proof: Proof. unfold poly_time_nonuniform_oc_func_2. exists (fun x o => o + 3*x). exists (fun x => 2 * x). intuition. eapply polynomial_plus; intuition. eapply polynomial_mult. eapply polynomial_const. eapply polynomial_ident. eapply polynomial_mult. eapply polynomial_const. eapply polynomial_ident. eapply cost_le. eapply cost_curry. eapply (PRFE_Encrypt_OC_cost_1 n). eapply (@PRFE_Encrypt_OC_cost_2 n); eauto. lia. eapply PRFE_Encrypt_OC_oc_cost; intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime Asymptotic