val mul_nat_helper (x y:nat) : Lemma (x * y >= 0)
let mul_nat_helper x y =
  FStar.Math.Lemmas.nat_times_nat_is_nat x y
val mul_nat_helper (x y:nat) : Lemma (x * y >= 0)
let mul_nat_helper x y =
FStar.Math.Lemmas.nat_times_nat_is_nat x y
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.nat FStar.Math.Lemmas.nat_times_nat_is_nat Prims.unit
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

type va_pbool = Vale.Def.PossiblyMonad.pbool
let va_ttrue () = Vale.Def.PossiblyMonad.ttrue
let va_ffalse = Vale.Def.PossiblyMonad.ffalse
let va_pbool_and x y = Vale.Def.PossiblyMonad.((&&.)) x y
val mul_nat_helper (x y:nat) : Lemma (x * y >= 0)
x: Prims.nat -> y: Prims.nat -> FStar.Pervasives.Lemma (ensures x * y >= 0)