proposition: Theorem IND_CPA_OI_impl_O : (IND_CPA_SecretKey_OI_Advantage <= maxA / 1 * IND_CPA_Adv)%rat.
proof: Proof. unfold IND_CPA_SecretKey_OI_Advantage. rewrite IND_CPA_SecretKey_OI_G0_Hybrid. rewrite IND_CPA_SecretKey_OI_G1_Hybrid. eapply leRat_trans. eapply Single_impl_ListHybrid. intuition. wftac. eapply oc_comp_wf_inv. eauto. intuition. unfold EncryptOracle; wftac. intuition. assert ((fun x => True) s'). trivial. eapply H3. simpl. trivial. 4:{ reflexivity. } intuition. wftac. unfold EncryptNothingOracle. eapply oc_comp_wf_inv. trivial. intuition. wftac. intuition. assert ((fun x => True) s'). trivial. eauto. simpl. trivial. intuition. intuition. eapply leRat_trans. 2:{ eapply IND_CPA_Adv_correct. } unfold DistSingle_Adv. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. apply IND_CPA_SecretKey_2Proc_impl_O. } unfold IND_CPA_SecretKey_O_3Proc_Advantage. eapply eqRat_impl_leRat. unfold DistSingle_G. unfold IND_CPA_SecretKey_O_3Proc_G0. eapply ratDistance_eqRat_compat; repeat (try comp_skip; try reflexivity; comp_simp; inline_first). Qed.
imports: FCF.FCF FCF.CompFold FCF.Hybrid