proposition: Theorem PRF_DRBG_G3_G4_close : | Pr[ PRF_DRBG_G3 ] - Pr[ PRF_DRBG_G4 ] | <= (l^2 / 2^eta).
proof: Proof. rewrite PRF_DRBG_G3_1_eq. rewrite PRF_DRBG_G3_1_2_eq. rewrite <- PRF_DRBG_G3_3_G4_eq. rewrite PRF_DRBG_G3_2_3_close. rewrite PRF_DRBG_G3_bad_equiv. rewrite PRF_DRBG_G3_bad_1_2_equiv. rewrite PRF_DRBG_G3_bad_2_3_equiv. rewrite PRF_DRBG_G3_bad_3_4_equiv. apply PRF_DRBG_G3_bad_4_small. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF