val lemma_disjoint_locations_symmetric (l1 l2: _)
    : Lemma (ensures ((!!(disjoint_locations l1 l2) = !!(disjoint_locations l2 l1))))
      (decreases %[L.length l1 + L.length l2])
let rec lemma_disjoint_locations_symmetric l1 l2 :
  Lemma
    (ensures (
        (!!(disjoint_locations l1 l2) = !!(disjoint_locations l2 l1))))
    (decreases %[L.length l1 + L.length l2]) =
  match l1, l2 with
  | [], [] -> ()
  | [], x :: xs | x :: xs, [] ->
    lemma_disjoint_locations_symmetric xs []
  | x :: xs, y :: ys ->
    lemma_disjoint_locations_symmetric l1 ys;
    lemma_disjoint_locations_symmetric xs l2;
    lemma_disjoint_locations_symmetric xs ys
val lemma_disjoint_locations_symmetric (l1 l2: _)
    : Lemma (ensures ((!!(disjoint_locations l1 l2) = !!(disjoint_locations l2 l1))))
      (decreases %[L.length l1 + L.length l2])
let rec lemma_disjoint_locations_symmetric l1 l2
    : Lemma (ensures ((!!(disjoint_locations l1 l2) = !!(disjoint_locations l2 l1))))
      (decreases %[L.length l1 + L.length l2]) =
match l1, l2 with
| [], [] -> ()
| [], x :: xs | x :: xs, [] -> lemma_disjoint_locations_symmetric xs []
| x :: xs, y :: ys ->
  lemma_disjoint_locations_symmetric l1 ys;
  lemma_disjoint_locations_symmetric xs l2;
  lemma_disjoint_locations_symmetric xs ys
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.locations FStar.Pervasives.Native.Mktuple2 Prims.list Vale.Transformers.Locations.location Vale.Transformers.Locations.lemma_disjoint_locations_symmetric Prims.Nil Prims.unit Prims.l_True Prims.squash Prims.b2t Prims.op_Equality Prims.bool Vale.Def.PossiblyMonad.op_Bang_Bang Vale.Transformers.Locations.disjoint_locations FStar.Pervasives.pattern
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] *)
let disjoint_location_from_locations (a:location) (l:locations) : pbool =
  for_all (fun b ->
      disjoint_location a b
    ) l

(** Disjointness of [locations] *)
let disjoint_locations (l1 l2:locations) : pbool =
  for_all (fun x ->
      disjoint_location_from_locations x l2
  ) l1

(** [disjoint_locations] is symmetric *)
let rec lemma_disjoint_locations_symmetric l1 l2 :
  Lemma
    (ensures (
        (!!(disjoint_locations l1 l2) = !!(disjoint_locations l2 l1))))
val lemma_disjoint_locations_symmetric (l1 l2: _)
    : Lemma (ensures ((!!(disjoint_locations l1 l2) = !!(disjoint_locations l2 l1))))
      (decreases %[L.length l1 + L.length l2])
l1: Vale.Transformers.Locations.locations -> l2: Vale.Transformers.Locations.locations
  -> FStar.Pervasives.Lemma
      (ensures
        !!(Vale.Transformers.Locations.disjoint_locations l1 l2) =
        !!(Vale.Transformers.Locations.disjoint_locations l2 l1))
      (decreases FStar.List.Tot.Base.length l1 + FStar.List.Tot.Base.length l2)