val i2s_map (#a:_) (#n:_) (il:interleaving a n) (i: SA.seq_index il)
  : (si:sseq_index (s_seq il){index il i = indexss (s_seq il) si /\ fst si = src il i})
val i2s_map (#a:_) (#n:_) (il:interleaving a n) (i: SA.seq_index il)
  : (si:sseq_index (s_seq il){index il i = indexss (s_seq il) si /\ fst si = src il i})
let i2s_map (#a:_) (#n:_) (il:interleaving a n) (i:seq_index il)
  = let t = src il i in
    let fm = seq_i_fm a n t in
    let j = IF.filter_map_map fm il i in
    IF.lemma_map_map #(gen_seq a n) (to_elem #a #n) il i;
    (t,j)
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)

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
/
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: Zeta.SeqAux.seq_index il
  -> si:
    Zeta.SSeq.sseq_index (Zeta.Interleave.s_seq il)
      { Zeta.Interleave.index il i = Zeta.SSeq.indexss (Zeta.Interleave.s_seq il) si /\
        FStar.Pervasives.Native.fst si = Zeta.Interleave.src il i }
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Zeta.Interleave.seq_index Zeta.Interleave.elem_src FStar.Pervasives.Native.Mktuple2 Prims.unit Zeta.IdxFn.lemma_map_map Zeta.Interleave.gen_seq Zeta.Interleave.to_elem Zeta.SeqAux.seq_index Zeta.IdxFn.filter_map Prims.l_and Prims.eq2 FStar.Seq.Base.index Zeta.IdxFn.__proj__FM__item__m Prims.b2t Prims.op_Equality Prims.l_or Prims.op_LessThan Zeta.IdxFn.flen Zeta.IdxFn.__proj__FM__item__f FStar.Seq.Base.length Zeta.IdxFn.idx2fidx Zeta.IdxFn.filter_map_map Zeta.IdxFn.fm_t Zeta.Interleave.seq_i_fm Zeta.Interleave.src Zeta.SSeq.sseq_index Zeta.Interleave.s_seq Zeta.Interleave.index Zeta.SSeq.indexss FStar.Pervasives.Native.fst
let i2s_map (#a #n: _) (il: interleaving a n) (i: seq_index il) =
  
let t = src il i in
let fm = seq_i_fm a n t in
let j = IF.filter_map_map fm il i in
IF.lemma_map_map #(gen_seq a n) (to_elem #a #n) il i;
(t, j)