val related_slots : slots: FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id ->
    i_slots: FStar.Seq.Base.seq Zeta.Steel.Rel.i_slot_id
  -> Prims.logical
let related_slots (slots: Seq.seq s_slot_id) (i_slots: Seq.seq i_slot_id)
  = let open FStar.Seq in
    length slots = length i_slots /\
    (forall i. related_slot (index slots i) (index i_slots i))
module Zeta.Steel.AppSim

open Zeta.Steel.ThreadStateModel
open Zeta.Steel.Rel
open Zeta.Steel.LogRel
open Zeta.Steel.StoreRel
open Zeta.Steel.ThreadRelDef
open Zeta.Steel.AddMRel
open FStar.Classical

module M = Zeta.Merkle
module R = Zeta.Record
module KU = Zeta.Steel.KeyUtils
module TSM = Zeta.Steel.ThreadStateModel
module GK = Zeta.GenKey
module IS = Zeta.Intermediate.Store

module A = Zeta.App
module AT = Zeta.Steel.ApplicationTypes
module T = Zeta.Steel.FormatsManual
module U16 = FStar.UInt16
module GV = Zeta.GenericVerifier
module IV = Zeta.Intermediate.Verifier

#push-options "--fuel 1 --ifuel 1 --query_stats"
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRelDef.fst.checked Zeta.Steel.StoreRel.fsti.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.LogRel.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.AddMRel.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.Merkle.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt16.fsti.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Steel.AppSim.fst

    slots: FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id ->
    i_slots: FStar.Seq.Base.seq Zeta.Steel.Rel.i_slot_id
  -> Prims.logical
FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id Zeta.Steel.Rel.i_slot_id Prims.l_and Prims.b2t Prims.op_Equality Prims.nat FStar.Seq.Base.length Prims.l_Forall Prims.op_LessThan Zeta.Steel.Rel.related_slot FStar.Seq.Base.index Prims.logical
let related_slots (slots: Seq.seq s_slot_id) (i_slots: Seq.seq i_slot_id) =
  
let open FStar.Seq in
length slots = length i_slots /\ (forall i. related_slot (index slots i) (index i_slots i))