let is_machine_heap_update (mh mh':machine_heap) =
  Set.equal (Map.domain mh) (Map.domain mh') /\
  (forall (i:int).{:pattern Map.sel mh i \/ Map.sel mh' i}
    not (Map.contains mh i) ==> Map.sel mh i == Map.sel mh' i)
let is_machine_heap_update (mh mh': machine_heap) =
Set.equal (Map.domain mh) (Map.domain mh') /\
(forall (i: int). {:pattern Map.sel mh i\/Map.sel mh' i}
    not (Map.contains mh i) ==> Map.sel mh i == Map.sel mh' i)
Vale.Arch.MachineHeap_s.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked
Vale.Arch.MachineHeap_s.fst
Vale.Arch.MachineHeap_s.machine_heap Prims.l_and FStar.Set.equal Prims.int FStar.Map.domain Vale.Def.Types_s.nat8 Prims.l_Forall Prims.l_imp Prims.b2t Prims.op_Negation FStar.Map.contains Prims.eq2 FStar.Map.sel Prims.logical
module Vale.Arch.MachineHeap_s

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd

let machine_heap = Map.t int nat8
val is_machine_heap_update : mh: Vale.Arch.MachineHeap_s.machine_heap -> mh': Vale.Arch.MachineHeap_s.machine_heap
  -> Prims.logical
mh: Vale.Arch.MachineHeap_s.machine_heap -> mh': Vale.Arch.MachineHeap_s.machine_heap
  -> Prims.logical