fact: Definition randomFunc_bad (s : list (D * R) * bool) d := [s, bad] <-2 s; match (arrayLookup _ s d) with | Some r => ret (r, (s, bad)) | None => r <-$ RndR; newF <- ((d, r) :: s); bad' <- fBad s d r; ret (r, (newF, bad || bad')) end.
imports: FCF PRF RndInList