val per_thread_prefix (#a:eqtype) (#n:nat) (il: interleaving a n) (i:nat{i <= length il})
  : Lemma (let ss = s_seq il in
           let il' = prefix il i in
           let ss' = s_seq il' in
           ss' `sseq_all_prefix_of` ss)
val per_thread_prefix (#a:eqtype) (#n:nat) (il: interleaving a n) (i:nat{i <= length il})
  : Lemma (let ss = s_seq il in
           let il' = prefix il i in
           let ss' = s_seq il' in
           ss' `sseq_all_prefix_of` ss)
let per_thread_prefix #a #n il i
  = let ss = s_seq il in
    let il' = prefix il i in
    let ss' = s_seq il' in
    let aux (t:_)
      : Lemma (ensures (S.index ss' t `prefix_of` S.index ss t))
      = IF.lemma_filter_map_prefix (seq_i_fm a n t) il i
    in
    forall_intro aux
module Zeta.Interleave

open FStar.Classical
open Zeta.SeqIdx

module IF = Zeta.IdxFn

let seq_index = SA.seq_index

let gen_seq (a:eqtype) (n:_) =
  {
    IF.a = elem_src a n;
    IF.phi = (fun _ -> True);
    IF.phi_commutes_with_prefix = (fun _ _ -> ());
  }

(* an element is from src t *)
let from_src #a #n (t: nat) (il: interleaving a n) (i: seq_index il)
  = t = (S.index il i).s

let to_elem #a #n (il: interleaving a n) (i: seq_index il)
  = (S.index il i).e

let i_seq (#a:_) (#n:nat) (il: interleaving a n)
  = IF.map #(gen_seq a n) (to_elem #a #n) il

let index_prop (#a #n:_) (il: interleaving a n) (i: SA.seq_index il)
  : Lemma (ensures ((S.index il i).e = index il i))
  = IF.lemma_map_map #(gen_seq a n) #_ to_elem il i

let seq_i_fm (a:eqtype) n (i:nat)
  : IF.fm_t (gen_seq a n) a
  = IF.FM (from_src #a #n i) (to_elem #a #n)

let s_seq_i (#a:_) (#n:_) (il: interleaving a n) (i:nat{i < n})
  = IF.filter_map (seq_i_fm a n i) il

let s_seq (#a:_) (#n:_) (il: interleaving a n)
  = init n (s_seq_i il)
/
Zeta.SSeq.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.IdxFn.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.Interleave.fst
il: Zeta.Interleave.interleaving a n -> i: Prims.nat{i <= FStar.Seq.Base.length il}
  -> FStar.Pervasives.Lemma
    (ensures
      (let ss = Zeta.Interleave.s_seq il in
        let il' = Zeta.Interleave.prefix il i in
        let ss' = Zeta.Interleave.s_seq il' in
        Zeta.SSeq.sseq_all_prefix_of ss' ss))
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.Interleave.elem_src FStar.Classical.forall_intro Prims.l_and Prims.op_LessThan FStar.Seq.Base.seq Zeta.SeqAux.prefix_of FStar.Seq.Base.index Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Zeta.IdxFn.lemma_filter_map_prefix Zeta.Interleave.gen_seq Zeta.Interleave.seq_i_fm Zeta.SSeq.sseq Prims.op_Equality Zeta.Interleave.s_seq Zeta.Interleave.prefix
let per_thread_prefix #a #n il i =
  
let ss = s_seq il in
let il' = prefix il i in
let ss' = s_seq il' in
let aux (t: _) : Lemma (ensures ((S.index ss' t) `prefix_of` (S.index ss t))) =
  IF.lemma_filter_map_prefix (seq_i_fm a n t) il i
in
forall_intro aux