val codes_modifies_ghost (cs: codes) : bool
val codes_modifies_ghost (cs: codes) : bool
let rec code_modifies_ghost (c:code) : bool =
  match c with
  | Ins (S.Ghost _) -> true
  | Ins _ -> false
  | Block cs -> codes_modifies_ghost cs
  | IfElse _ c1 c2 -> code_modifies_ghost c1 || code_modifies_ghost c2
  | While _ c -> code_modifies_ghost c
and codes_modifies_ghost (cs:codes) : bool =
  match cs with
  | [] -> false
  | c::cs -> code_modifies_ghost c || codes_modifies_ghost cs
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
let xer_ca (xer:xer_t) : bool = S.xer_ca xer
let update_xer_ov (xer:xer_t) (new_xer_ov:bool) = S.update_xer_ov xer new_xer_ov
let update_xer_ca (xer:xer_t) (new_xer_ca:bool) = S.update_xer_ca xer new_xer_ca
/
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
cs: Vale.PPC64LE.Lemmas.codes -> Prims.bool
Vale.PPC64LE.Lemmas.codes Vale.PPC64LE.Semantics_s.code Prims.list Prims.op_BarBar Vale.PPC64LE.Lemmas.code_modifies_ghost Vale.PPC64LE.Lemmas.codes_modifies_ghost Prims.bool
let rec codes_modifies_ghost (cs: codes) : bool =
  
match cs with
| [] -> false
| c :: cs -> code_modifies_ghost c || codes_modifies_ghost cs