val 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))
val 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 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))
  )
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)
/
prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.SeqMachine.fst

    sm: Zeta.SeqMachine.seq_machine ->
    s: FStar.Seq.Base.seq (Zeta.SeqMachine.elem_type sm) {Zeta.SeqMachine.valid sm s} ->
    i: Prims.nat{i <= FStar.Seq.Base.length s}
  -> FStar.Pervasives.Lemma (ensures Zeta.SeqMachine.valid sm (Zeta.SeqAux.prefix s i))
Zeta.SeqMachine.seq_machine FStar.Seq.Base.seq Zeta.SeqMachine.elem_type Prims.b2t Zeta.SeqMachine.valid Prims.nat Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.bool Zeta.SeqAux.lemma_reduce_identity Zeta.SeqMachine.state_type Zeta.SeqMachine.fail_state Zeta.SeqMachine.trans_fn Zeta.SeqAux.suffix Prims.op_Subtraction Prims.unit Zeta.SeqAux.lemma_reduce_prefix Zeta.SeqMachine.init_state Prims.op_Equality Zeta.SeqAux.prefix Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern
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)))