val va_ttrue (_:unit) : va_pbool
let va_ttrue () = Vale.Def.PossiblyMonad.ttrue
val va_ttrue (_:unit) : va_pbool
let va_ttrue () =
Vale.Def.PossiblyMonad.ttrue
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
Prims.unit Vale.Def.PossiblyMonad.ttrue Vale.PPC64LE.Decls.va_pbool
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
let xer_ca = Lemmas.xer_ca
let update_xer_ov = Lemmas.update_xer_ov
let update_xer_ca = Lemmas.update_xer_ca
let ins = S.ins
type ocmp = S.ocmp
type va_fuel = nat
val va_ttrue (_:unit) : va_pbool
_: Prims.unit -> Vale.PPC64LE.Decls.va_pbool