proposition: Theorem PRF_NA_impl_NAI : PRF_NAI_Advantage <= (maxLists / 1 * maxDistance)%rat.
proof: Proof. rewrite PRF_NAI_Advantage_eq_Hybrid. rewrite Single_impl_ListHybrid. reflexivity. intuition. wftac. intuition. wftac. eapply oracleMap_wf. intuition. eapply randomFunc_wf; intuition. intuition. intuition. assert (DistSingle_Adv (fun lsD : list D => k <-$ RndKey; ret map (f k) lsD) (fun lsD : list D => z <-$ oracleMap (list_EqDec (pair_EqDec D_EqDec R_EqDec)) R_EqDec RndR_func nil lsD; [lsR, _]<-2 z; ret lsR) (B1 nil (list_EqDec D_EqDec) A_state_EqDec A1 i) (B2 (fun lsD : list D => k <-$ RndKey; ret map (f k) lsD) (fun lsD : list D => z <-$ oracleMap (list_EqDec (pair_EqDec D_EqDec R_EqDec)) R_EqDec RndR_func nil lsD; [lsR, _]<-2 z; ret lsR) (list_EqDec R_EqDec) A2) == PRF_NA_Advantage (B1 nil (list_EqDec D_EqDec) A_state_EqDec A1 i) (B2 (fun lsD : list D => k <-$ RndKey; ret map (f k) lsD) (fun lsD : list D => z <-$ oracleMap (list_EqDec (pair_EqDec D_EqDec R_EqDec)) R_EqDec RndR_func nil lsD; [lsR, _]<-2 z; ret lsR) (list_EqDec R_EqDec) A2) ). unfold DistSingle_Adv, PRF_NA_Advantage, DistSingle_G, PRF_NA_G_A, PRF_NA_G_B. eapply ratDistance_eqRat_compat; repeat (try comp_skip; try reflexivity; comp_simp; inline_first). rewrite H. clear H. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid