fact: Definition emergencyBreak (x : Blist)(oracle : P_oracle) := n <-$ [0 .. d); b <-$ oracle _ (fun a resp => [e, z] <-$2 queryRow resp x a; ret (V_accept x a e z)); ret (b && eqb n O).
imports: Crypto FCF RndNat Asymptotic