val is_blum_add_epoch : ep: Zeta.Time.epoch ->
    il: Zeta.Generic.Interleave.verifiable_log vspec n ->
    i: Zeta.Generic.Interleave.seq_index il
  -> Prims.bool
let is_blum_add_epoch (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (i: seq_index il)
  = is_blum_add il i &&
    (let be = blum_add_elem il i in
     be.t.e = ep)
module Zeta.Generic.Blum

open Zeta.Interleave
open Zeta.MultiSet
open Zeta.GenKey
open Zeta.Time
open Zeta.MultiSetHashDomain
open Zeta.GenericVerifier
open Zeta.Generic.Interleave
open Zeta.Generic.TSLog

module I = Zeta.Interleave
module S = FStar.Seq
module SA = Zeta.SeqAux
module G = Zeta.Generic.Global
/
Zeta.Time.fsti.checked Zeta.SeqAux.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Interleave.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.TSLog.fsti.checked Zeta.Generic.Interleave.fsti.checked Zeta.Generic.Global.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.Generic.Blum.fsti

    ep: Zeta.Time.epoch ->
    il: Zeta.Generic.Interleave.verifiable_log vspec n ->
    i: Zeta.Generic.Interleave.seq_index il
  -> Prims.bool
Zeta.GenericVerifier.verifier_spec Prims.nat Zeta.Time.epoch Zeta.Generic.Interleave.verifiable_log Zeta.Generic.Interleave.seq_index Prims.op_AmpAmp Zeta.Generic.Interleave.is_blum_add Prims.op_Equality Zeta.Time.__proj__Mktimestamp__item__e Zeta.MultiSetHashDomain.__proj__MHDom__item__t Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.Generic.Interleave.blum_add_elem Prims.bool
let is_blum_add_epoch (#vspec #n: _) (ep: epoch) (il: verifiable_log vspec n) (i: seq_index il) =
  
is_blum_add il i &&
(let be = blum_add_elem il i in
  be.t.e = ep)