val consistent_log_implies_hprefix_consistent
      (#vcfg: _)
      (init_map: slot_state_map vcfg)
      (l: logS vcfg {length l > 0})
    : Lemma (requires (consistent_log init_map l))
      (ensures
        (let i = length l - 1 in
          let l' = prefix l i in
          consistent_log init_map l'))
      [SMTPat (consistent_log init_map l)]
val consistent_log_implies_hprefix_consistent
      (#vcfg: _)
      (init_map: slot_state_map vcfg)
      (l: logS vcfg {length l > 0})
    : Lemma (requires (consistent_log init_map l))
      (ensures
        (let i = length l - 1 in
          let l' = prefix l i in
          consistent_log init_map l'))
      [SMTPat (consistent_log init_map l)]
let consistent_log_implies_hprefix_consistent (#vcfg:_) (init_map: slot_state_map vcfg) (l: logS vcfg {length l > 0})
  : Lemma (requires (consistent_log init_map l))
          (ensures (let i = length l - 1 in
                    let l' = prefix l i in
                    consistent_log init_map l'))
          [SMTPat (consistent_log init_map l)]
  = let i = length l - 1 in
    let l' = prefix l i in
    let aux(s:_)
      : Lemma (ensures (slot_state_trans_closure s l' (init_map s) <> None))
      = eliminate forall (s:slot_id vcfg). slot_state_trans_closure s l (init_map s) <> None
        with s
    in
    forall_intro aux
module Zeta.Intermediate.Logs

open FStar.Classical
open Zeta.SeqIdx

let all_slots_assoc_comp (#vcfg:_) (ssm: slot_state_map vcfg) (ss: seq (slot_id vcfg))
  : b:bool{b <==> all_slots_assoc ssm ss}
  = not (exists_elems_with_prop_comp (fun s -> not (is_assoc ssm s)) ss)

#push-options "--fuel 1 --ifuel 1 --query_stats"
/
Zeta.SeqIdx.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Intermediate.Logs.fst

    init_map: Zeta.Intermediate.SlotKeyRel.slot_state_map vcfg ->
    l: Zeta.Intermediate.Logs.logS vcfg {FStar.Seq.Base.length l > 0}
  -> FStar.Pervasives.Lemma (requires Zeta.Intermediate.Logs.consistent_log init_map l)
      (ensures
        (let i = FStar.Seq.Base.length l - 1 in
          let l' = Zeta.SeqAux.prefix l i in
          Zeta.Intermediate.Logs.consistent_log init_map l'))
      [SMTPat (Zeta.Intermediate.Logs.consistent_log init_map l)]
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.SlotKeyRel.slot_state_map Zeta.Intermediate.Logs.logS Prims.b2t Prims.op_GreaterThan FStar.Seq.Base.length Zeta.Intermediate.Verifier.logS_entry FStar.Classical.forall_intro Zeta.Intermediate.VerifierConfig.slot_id Prims.op_disEquality FStar.Pervasives.Native.option Zeta.Intermediate.SlotKeyRel.slot_state Zeta.Intermediate.Logs.slot_state_trans_closure FStar.Pervasives.Native.None Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern FStar.Classical.Sugar.forall_elim FStar.Seq.Base.seq Prims.op_Equality Prims.nat Zeta.SeqAux.prefix Prims.int Prims.op_Subtraction Zeta.Intermediate.Logs.consistent_log Prims.Cons FStar.Pervasives.smt_pat Prims.logical
let consistent_log_implies_hprefix_consistent
      (#vcfg: _)
      (init_map: slot_state_map vcfg)
      (l: logS vcfg {length l > 0})
    : Lemma (requires (consistent_log init_map l))
      (ensures
        (let i = length l - 1 in
          let l' = prefix l i in
          consistent_log init_map l'))
      [SMTPat (consistent_log init_map l)] =
  
let i = length l - 1 in
let l' = prefix l i in
let aux (s: _) : Lemma (ensures (slot_state_trans_closure s l' (init_map s) <> None)) =
  eliminate forall (s: slot_id vcfg). slot_state_trans_closure s l (init_map s) <> None
  with s
in
forall_intro aux