val max_valid_prefix (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))))
              })
val max_valid_prefix (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))))
              })
let max_valid_prefix = max_valid_prefix_aux
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))
/
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)
  -> 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.max_valid_prefix_aux
let max_valid_prefix =
  
max_valid_prefix_aux