proposition: Theorem G5_one_half : Pr[G5] == 1/2.
proof: Proof. pose proof @RF_Encrypt_wf as RF_Encrypt_wf. unfold G5. comp_irr_l. eapply oc_comp_wf; intuition. comp_simp. do 3 (comp_irr_l; wftac). eapply oc_comp_wf; intuition. comp_simp. Transparent evalDist. Transparent getSupport. dist_compute. Opaque evalDist. Opaque getSupport. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime