val lemma_empty_seq_valid_all (psm: pseq_machine):
  Lemma (valid_all psm (empty #(elem_type_p psm)))
val lemma_empty_seq_valid_all (psm: pseq_machine):
  Lemma (valid_all psm (empty #(elem_type_p psm)))
let lemma_empty_seq_valid_all (psm: pseq_machine):
  Lemma (valid_all psm (empty #(elem_type_p psm))) =
  let s = empty #(elem_type_p psm) in
  let key = key_type psm in
  let sm = seq_machine_of psm in
  let pf = partn_fn psm in
  let aux(k: key):
    Lemma (requires True)
          (ensures (valid sm (partn psm k s)))
          [SMTPat (valid sm (partn psm k s))]
          =
    lemma_filter_empty (iskey pf k);
    lemma_empty_seq_valid sm
  in
  ()
module Zeta.SeqMachine

let lemma_empty_seq_init (sm: seq_machine) (s: seq (elem_type sm){length s = 0})
  : Lemma (ensures (seq_machine_run sm s = (init_state sm)))
  = lemma_reduce_empty (init_state sm) (trans_fn sm);
    lemma_empty s

let lemma_empty_seq_valid (sm: seq_machine):
  Lemma (valid sm (empty #(elem_type sm))) =
  lemma_reduce_empty (init_state sm) (trans_fn sm)

let lemma_valid_prefix (sm: seq_machine) (s: (seq (elem_type sm)){valid sm s}) (i:nat{i <= length s}):
  Lemma (valid sm (prefix s i)) =
  let si = prefix s i in
  if valid sm si then ()
  else (
    lemma_reduce_prefix (init_state sm) (trans_fn sm) s i;
    lemma_reduce_identity (fail_state sm) (trans_fn sm) (suffix s (length s - i))
  )

let rec max_valid_prefix_aux (sm: seq_machine) (s: seq (elem_type sm))
  : Tot (i:nat{i <= length s /\
              valid sm (prefix s i) /\
              (i < length s ==> not (valid sm (prefix s (i + 1))))
              })
    (decreases (length s)) =
  lemma_empty_seq_valid sm;
  lemma_prefix0_empty s;
  let n = length s in
  if valid sm s then n
  else max_valid_prefix_aux sm (prefix s (n - 1))

let max_valid_prefix = max_valid_prefix_aux
/
prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.SeqMachine.fst
psm: Zeta.SeqMachine.pseq_machine
  -> FStar.Pervasives.Lemma (ensures Zeta.SeqMachine.valid_all psm FStar.Seq.Base.empty)
Zeta.SeqMachine.pseq_machine Prims.unit Prims.l_True Prims.squash Prims.b2t Zeta.SeqMachine.valid Zeta.SeqMachine.partn Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.bool Prims.Nil Zeta.SeqMachine.lemma_empty_seq_valid Zeta.SeqAux.lemma_filter_empty Zeta.SeqMachine.elem_type_p Zeta.SeqMachine.iskey Zeta.SeqMachine.key_type Zeta.SeqMachine.partn_fn Zeta.SeqMachine.seq_machine Zeta.SeqMachine.seq_machine_of Prims.eqtype FStar.Seq.Base.seq Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Seq.Base.empty Zeta.SeqMachine.valid_all
let lemma_empty_seq_valid_all (psm: pseq_machine) : Lemma (valid_all psm (empty #(elem_type_p psm))) =
  
let s = empty #(elem_type_p psm) in
let key = key_type psm in
let sm = seq_machine_of psm in
let pf = partn_fn psm in
let aux (k: key)
    : Lemma (requires True) (ensures (valid sm (partn psm k s))) [SMTPat (valid sm (partn psm k s))]
=
  lemma_filter_empty (iskey pf k);
  lemma_empty_seq_valid sm
in
()