proposition: Theorem PRFE_Encrypt_OC_cost_2 : forall x, cost (PRFE_Encrypt_OC x) (2 * eta).
proof: Proof. intuition. Transparent PRFE_Encrypt_OC. unfold PRFE_Encrypt_OC. eapply cost_le. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_compose_unary; costtac. eapply cost_compose_unary; costtac. eapply cost_compose_binary; costtac. eapply cost_compose_binary; costtac. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_BVxor. intuition. eapply cost_uncurry_2. eapply cost_BVxor. lia. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime