val is_blum_add_ifn (#vspec #n: _) : IF.idxfn_t (gen_seq vspec n) bool
val is_blum_add_ifn (#vspec #n: _) : IF.idxfn_t (gen_seq vspec n) bool
let is_blum_add_ifn (#vspec #n:_)
  : IF.idxfn_t (gen_seq vspec n) bool
  = is_blum_add #vspec #n
module Zeta.Generic.Blum

open Zeta.Ghost
open Zeta.SMap
open FStar.Classical

module IF = Zeta.IdxFn
module T = Zeta.Generic.Thread

let gen_seq (vspec:verifier_spec) (n:_) = {
  IF.a = I.elem_src (verifier_log_entry vspec) n;
  IF.phi = verifiable;
  IF.phi_commutes_with_prefix = (fun il i -> lemma_prefix_verifiable n il i);
}

let is_blum_add_epoch_ifn (#vspec #n:_) (ep: epoch)
  : IF.idxfn_t (gen_seq vspec n) bool
  = is_blum_add_epoch #vspec #n ep
/
Zeta.SMap.fsti.checked Zeta.MultiSet.SSeq.fsti.checked Zeta.IdxFn.fsti.checked Zeta.Ghost.fsti.checked Zeta.Generic.Thread.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Generic.Blum.fst
Zeta.IdxFn.idxfn_t (Zeta.Generic.Blum.gen_seq vspec n) Prims.bool
Zeta.GenericVerifier.verifier_spec Prims.nat Zeta.Generic.Interleave.is_blum_add Zeta.IdxFn.idxfn_t Zeta.Generic.Blum.gen_seq Prims.bool
let is_blum_add_ifn (#vspec #n: _) : IF.idxfn_t (gen_seq vspec n) bool =
  
is_blum_add #vspec #n