val cond_idxfn_t : b: Type0 -> f: Zeta.IdxFn.idxfn_t gs Prims.bool -> Type0
let cond_idxfn_t (#gs:_) (b:Type0) (f:idxfn_t gs bool) =
  m:cond_idxfn_t_base b f{cond_prefix_property m}
module Zeta.IdxFn

open FStar.Seq
open Zeta.SeqAux
module SA = Zeta.SeqAux

noeq
type gen_seq_spec = {
  a : eqtype;
  phi : Seq.seq a -> Type0;
  phi_commutes_with_prefix :
    s:Seq.seq a{phi s} ->
    i:nat{i <= Seq.length s} ->
    Lemma (phi (SA.prefix s i));
}

type seq_t (gs:gen_seq_spec) = s:Seq.seq gs.a{gs.phi s}

let prefix (#gs:gen_seq_spec) (s:seq_t gs) (i:nat{i <= Seq.length s})
  : seq_t gs
  = gs.phi_commutes_with_prefix s i;
    SA.prefix s i

let seq_index (#gs: gen_seq_spec) (s: seq_t gs) = i:nat{i < Seq.length s}

(* an index function is a function that maps indexed elements of a sequence to another domain. *)
type idxfn_t_base (gs: gen_seq_spec) (b:Type0) =
  s:seq_t gs -> i:seq_index s -> b

(* an index function has a prefix property if the value of the function at an index depends only on the
 * sequence until that index *)
let prefix_property
  (#gs:_)
  (#b:_)
  (f: idxfn_t_base gs b)
  = forall (s: seq_t gs) (i: seq_index s) (j: nat).
    {:pattern f (prefix s j) i}
    j <= Seq.length s ==>
    i < j ==>
    f s i == f (prefix s j) i

(* an index function with the prefix property *)
type idxfn_t (gs:_) (b:_) = f:idxfn_t_base gs b {prefix_property f}

(* conjunction of two index filters *)
let conj #gs (f1 f2: idxfn_t gs bool) : idxfn_t gs bool =
  fun (s: seq_t gs) (i: seq_index s) ->
  f1 s i && f2 s i

(* a conditional index function is a function that is defined only some indexes satisfying
 * a predicate *)
type cond_idxfn_t_base (#gs:_) (b:Type0) (f:idxfn_t gs bool) =
  s:seq_t gs -> i:seq_index s{f s i} -> b

unfold
let cond_prefix_property
  (#gs:_)
  (#b:_)
  (#f:idxfn_t gs bool)
  (m: cond_idxfn_t_base b f)
  = forall (s: seq_t gs) (i:seq_index s) (j: nat).
    {:pattern m (prefix s j) i}
    j <= Seq.length s ==>
    i < j ==>
    f s i ==>
    m s i == m (prefix s j) i
/
Zeta.SeqAux.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.IdxFn.fsti
b: Type0 -> f: Zeta.IdxFn.idxfn_t gs Prims.bool -> Type0
Zeta.IdxFn.gen_seq_spec Zeta.IdxFn.idxfn_t Prims.bool Zeta.IdxFn.cond_idxfn_t_base Zeta.IdxFn.cond_prefix_property
let cond_idxfn_t (#gs: _) (b: Type0) (f: idxfn_t gs bool) =
  
m: cond_idxfn_t_base b f {cond_prefix_property m}