val update_xer_ov (xer:xer_t) (new_xer_ov:bool) : xer_t
let update_xer_ov = Lemmas.update_xer_ov
val update_xer_ov (xer:xer_t) (new_xer_ov:bool) : xer_t
let update_xer_ov =
Lemmas.update_xer_ov
Vale.PPC64LE.Decls.fst.checked
Vale.PPC64LE.StateLemmas.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Print_s.fst.checked Vale.PPC64LE.Memory_Sems.fsti.checked Vale.PPC64LE.Memory.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.Lemmas.fsti.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.IO.fst.checked
Vale.PPC64LE.Decls.fst
Vale.PPC64LE.Lemmas.update_xer_ov
module Vale.PPC64LE.Decls
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.StateLemmas
module S = Vale.PPC64LE.Semantics_s
module P = Vale.PPC64LE.Print_s
friend Vale.PPC64LE.Memory

let same_heap_types = ()

let xer_ov = Lemmas.xer_ov
val update_xer_ov (xer:xer_t) (new_xer_ov:bool) : xer_t
xer: Vale.PPC64LE.Machine_s.xer_t -> new_xer_ov: Prims.bool -> Vale.PPC64LE.Machine_s.xer_t