val create_heaplets_this (buffers: list buffer_info) (s: state) : GTot state
let create_heaplets_this (buffers:list buffer_info) (s:state) : GTot state =
  {s with ms_heap = Vale.PPC64LE.Memory_Sems.create_heaplets buffers s.ms_heap}
val create_heaplets_this (buffers: list buffer_info) (s: state) : GTot state
let create_heaplets_this (buffers: list buffer_info) (s: state) : GTot state =
{ s with ms_heap = Vale.PPC64LE.Memory_Sems.create_heaplets buffers s.ms_heap }
Vale.PPC64LE.InsMem.fst.checked
Vale.PPC64LE.StateLemmas.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory_Sems.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fst.checked Vale.PPC64LE.Decls.fst.checked Vale.Lib.Seqs.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.PPC64LE.InsMem.fst
Prims.list Vale.Arch.HeapImpl.buffer_info Vale.PPC64LE.State.state Vale.PPC64LE.Machine_s.Mkstate Vale.PPC64LE.Machine_s.__proj__Mkstate__item__ok Vale.PPC64LE.Machine_s.__proj__Mkstate__item__regs Vale.PPC64LE.Machine_s.__proj__Mkstate__item__vecs Vale.PPC64LE.Machine_s.__proj__Mkstate__item__cr0 Vale.PPC64LE.Machine_s.__proj__Mkstate__item__xer Vale.PPC64LE.Memory_Sems.create_heaplets Vale.PPC64LE.Machine_s.__proj__Mkstate__item__ms_heap Vale.PPC64LE.Machine_s.__proj__Mkstate__item__ms_stack Vale.PPC64LE.Machine_s.__proj__Mkstate__item__ms_stackTaint
module Vale.PPC64LE.InsMem
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.StateLemmas
open Vale.PPC64LE.Decls
open Vale.PPC64LE.InsBasic
open Vale.Arch.Heap
open Vale.Arch.HeapImpl
module S = Vale.PPC64LE.Semantics_s

friend Vale.PPC64LE.Decls
#reset-options "--initial_fuel 2 --max_fuel 2 --max_ifuel 2 --z3rlimit 20"
val create_heaplets_this (buffers: list buffer_info) (s: state) : GTot state
buffers: Prims.list Vale.Arch.HeapImpl.buffer_info -> s: Vale.PPC64LE.State.state
  -> Prims.GTot Vale.PPC64LE.State.state