val disjoint_location_from_locations (a: location) (l: locations) : pbool
let disjoint_location_from_locations (a:location) (l:locations) : pbool =
  for_all (fun b ->
      disjoint_location a b
    ) l
val disjoint_location_from_locations (a: location) (l: locations) : pbool
let disjoint_location_from_locations (a: location) (l: locations) : pbool =
for_all (fun b -> disjoint_location a b) l
Vale.Transformers.Locations.fsti.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.Universe.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.FunctionalExtensionality.fsti.checked
Vale.Transformers.Locations.fsti
Vale.Transformers.Locations.location Vale.Transformers.Locations.locations Vale.Def.PossiblyMonad.for_all Vale.Transformers.Locations.disjoint_location Vale.Def.PossiblyMonad.pbool
module Vale.Transformers.Locations

open Vale.X64.Bytes_Code_s
open Vale.X64.Instruction_s
open Vale.X64.Instructions_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.X64.Print_s

open Vale.Def.PossiblyMonad

module L = FStar.List.Tot

(** An [location] is a portion of the [machine_state] that may be
    independently modified and/or accessed. *)
val location : eqtype

unfold
type locations = list location

(** [disjoint_location a1 a2] is true whenever locations [a1] and [a2]
    are disjoint. When not disjoint, it gives a reason for why not. *)
val disjoint_location : location -> location -> pbool

(** Disjointness is the same as syntactic equality on the locations. *)
val auto_lemma_disjoint_location :
  a1:location -> a2:location ->
  Lemma
    (ensures (!!(disjoint_location a1 a2) = (a1 <> a2)))
    [SMTPat (!!(disjoint_location a1 a2))]

(** Disjointness of a [location] from [locations] *)
val disjoint_location_from_locations (a: location) (l: locations) : pbool
a: Vale.Transformers.Locations.location -> l: Vale.Transformers.Locations.locations
  -> Vale.Def.PossiblyMonad.pbool