val lemma_spec_rel_implies_same_add_elem (#vcfg:_)
  (il: verifiable_log vcfg {spec_rel il})
  (i: seq_index il {is_blum_add il i})
  : Lemma (ensures (let ilk = to_logk il in
                    is_blum_add ilk i /\
                    blum_add_elem il i = blum_add_elem ilk i))
          [SMTPat (blum_add_elem il i)]
val lemma_spec_rel_implies_same_add_elem (#vcfg:_)
  (il: verifiable_log vcfg {spec_rel il})
  (i: seq_index il {is_blum_add il i})
  : Lemma (ensures (let ilk = to_logk il in
                    is_blum_add ilk i /\
                    blum_add_elem il i = blum_add_elem ilk i))
          [SMTPat (blum_add_elem il i)]
let lemma_spec_rel_implies_same_add_elem (#vcfg:_)
  (il: verifiable_log vcfg {spec_rel il})
  (i: seq_index il {is_blum_add il i})
  : Lemma (ensures (let ilk = to_logk il in
                    is_blum_add ilk i /\
                    blum_add_elem il i = blum_add_elem ilk i))
  = lemma_spec_rel_implies_prefix_spec_rel il i
module Zeta.Intermediate.Blum

open Zeta.Intermediate.Store
open Zeta.Intermediate.StateRel
open FStar.Classical

module SA = Zeta.SeqAux
module GV = Zeta.GenericVerifier
module HV = Zeta.High.Verifier
module IV = Zeta.Intermediate.Verifier

#push-options "--fuel 0 --ifuel 1 --query_stats"
/
Zeta.SeqAux.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.Intermediate.StateRel.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenericVerifier.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Zeta.Intermediate.Blum.fst

    il: Zeta.Intermediate.Interleave.verifiable_log vcfg {Zeta.Intermediate.Interleave.spec_rel il} ->
    i: Zeta.Generic.Interleave.seq_index il {Zeta.Generic.Interleave.is_blum_add il i}
  -> FStar.Pervasives.Lemma
      (ensures
        (let ilk = Zeta.Intermediate.Interleave.to_logk il in
          Zeta.Generic.Interleave.is_blum_add ilk i /\
          Zeta.Generic.Interleave.blum_add_elem il i = Zeta.Generic.Interleave.blum_add_elem ilk i))
      [SMTPat (Zeta.Generic.Interleave.blum_add_elem il i)]
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Interleave.verifiable_log Zeta.Intermediate.Interleave.spec_rel Zeta.Generic.Interleave.seq_index Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__thread_count Prims.b2t Zeta.Generic.Interleave.is_blum_add Zeta.Intermediate.Interleave.lemma_spec_rel_implies_prefix_spec_rel Prims.unit Prims.l_True Prims.squash Prims.l_and Zeta.High.Verifier.high_verifier_spec Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Prims.op_Equality Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Generic.Interleave.blum_add_elem Zeta.High.Interleave.ilog Zeta.Intermediate.Interleave.to_logk Prims.Nil FStar.Pervasives.pattern
let lemma_spec_rel_implies_same_add_elem
      (#vcfg: _)
      (il: verifiable_log vcfg {spec_rel il})
      (i: seq_index il {is_blum_add il i})
    : Lemma
    (ensures
      (let ilk = to_logk il in
        is_blum_add ilk i /\ blum_add_elem il i = blum_add_elem ilk i)) =
  
lemma_spec_rel_implies_prefix_spec_rel il i