val update_xer_ov : xer: Vale.PPC64LE.Machine_s.xer_t -> new_xer_ov: Prims.bool
  -> new_xer: Vale.PPC64LE.Machine_s.xer_t{Vale.PPC64LE.Semantics_s.xer_ov new_xer == new_xer_ov}
let update_xer_ov (xer:xer_t) (new_xer_ov:bool) = S.update_xer_ov xer new_xer_ov
module Vale.PPC64LE.Lemmas
open Vale.Def.Prop_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.StateLemmas
module S = Vale.PPC64LE.Semantics_s
open Vale.Arch.Heap
open Vale.Arch.HeapImpl
open Vale.Arch.HeapLemmas

unfold let code = S.code
unfold let codes = S.codes
unfold let ocmp = S.ocmp
unfold let fuel = nat

let xer_ov (xer:xer_t) : bool = S.xer_ov xer
/
Vale.PPC64LE.StateLemmas.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapLemmas.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.PPC64LE.Lemmas.fsti
xer: Vale.PPC64LE.Machine_s.xer_t -> new_xer_ov: Prims.bool
  -> new_xer: Vale.PPC64LE.Machine_s.xer_t{Vale.PPC64LE.Semantics_s.xer_ov new_xer == new_xer_ov}
Vale.PPC64LE.Machine_s.xer_t Prims.bool Vale.PPC64LE.Semantics_s.update_xer_ov Prims.eq2 Vale.PPC64LE.Semantics_s.xer_ov
let update_xer_ov (xer: xer_t) (new_xer_ov: bool) =
  
S.update_xer_ov xer new_xer_ov