val 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))
val 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))
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))
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))
  )
/
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)
  -> Prims.Tot
    (i:
      Prims.nat
        { i <= FStar.Seq.Base.length s /\ Zeta.SeqMachine.valid sm (Zeta.SeqAux.prefix s i) /\
          (i < FStar.Seq.Base.length s ==>
            Prims.op_Negation (Zeta.SeqMachine.valid sm (Zeta.SeqAux.prefix s (i + 1)))) })
Zeta.SeqMachine.seq_machine FStar.Seq.Base.seq Zeta.SeqMachine.elem_type Zeta.SeqMachine.valid Prims.bool Zeta.SeqMachine.max_valid_prefix_aux Zeta.SeqAux.prefix Prims.op_Subtraction Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.l_imp Prims.op_LessThan Prims.op_Negation Prims.op_Addition Prims.unit Zeta.SeqAux.lemma_prefix0_empty Zeta.SeqMachine.lemma_empty_seq_valid
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))