proposition: Theorem RPS_G_1_bad_small : Pr [x <-$ RPS_G_1; ret snd x ] <= A2_queries / 1 * badProb A2_queries.
proof: Proof. unfold RPS_G_1. inline_first. assert (Pr [a <-$ A2 (list (D * R) * bool)%type _ (randomFunc_bad) (nil, false); x <-$ ([b, s]<-2 a; ret (b, snd s)); ret snd x ] == Pr [a <-$ A2 (list (D * R) * bool)%type _ (randomFunc_bad) (nil, false); ret snd (snd a) ] ). comp_skip. comp_simp. reflexivity. rewrite H. clear H. eapply leRat_trans. eapply (@oc_eventProb_0_1 _ (fun p => length (fst p)) _ badProb). eauto. eapply badProb_mono. trivial. intuition. simpl in *. subst. case_eq (arrayLookup eqdd a a0); intuition. comp_simp. simpl. rewrite evalDist_ret_0. eapply rat0_le_all. congruence. simpl in *. eapply leRat_trans. 2:{ eapply badProb_correct. } inline_first. comp_skip. simpl. eapply leRat_refl. intuition. simpl in *. destruct (arrayLookup eqdd a a1); repeat simp_in_support. lia. simpl. intuition. trivial. intuition. Qed.
imports: FCF PRF RndInList