val lemma_empty_seq_valid (sm: seq_machine):
  Lemma (valid sm (empty #(elem_type sm)))
val lemma_empty_seq_valid (sm: seq_machine):
  Lemma (valid sm (empty #(elem_type sm)))
let lemma_empty_seq_valid (sm: seq_machine):
  Lemma (valid sm (empty #(elem_type sm))) =
  lemma_reduce_empty (init_state sm) (trans_fn sm)
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
/
prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.SeqMachine.fst
sm: Zeta.SeqMachine.seq_machine
  -> FStar.Pervasives.Lemma (ensures Zeta.SeqMachine.valid sm FStar.Seq.Base.empty)
Zeta.SeqMachine.seq_machine Zeta.SeqAux.lemma_reduce_empty Zeta.SeqMachine.elem_type Zeta.SeqMachine.state_type Zeta.SeqMachine.init_state Zeta.SeqMachine.trans_fn Prims.unit Prims.l_True Prims.squash Prims.b2t Zeta.SeqMachine.valid FStar.Seq.Base.empty Prims.Nil FStar.Pervasives.pattern
let lemma_empty_seq_valid (sm: seq_machine) : Lemma (valid sm (empty #(elem_type sm))) =
  
lemma_reduce_empty (init_state sm) (trans_fn sm)