val 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)))
val 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)))
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
module Zeta.SeqMachine
/
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) {FStar.Seq.Base.length s = 0}
  -> FStar.Pervasives.Lemma
    (ensures Zeta.SeqMachine.seq_machine_run sm s = Zeta.SeqMachine.init_state sm)
Zeta.SeqMachine.seq_machine FStar.Seq.Base.seq Zeta.SeqMachine.elem_type Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Seq.Base.lemma_empty Prims.unit Zeta.SeqAux.lemma_reduce_empty Zeta.SeqMachine.state_type Zeta.SeqMachine.init_state Zeta.SeqMachine.trans_fn Prims.l_True Prims.squash Zeta.SeqMachine.seq_machine_run Prims.Nil FStar.Pervasives.pattern
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