val loc_includes_union_assoc_focalize_2
  (l x r1 r2 s: loc)
: Lemma
  (requires (loc_includes (loc_union l (loc_union x (loc_union r1 r2))) s))
  (ensures (loc_includes (loc_union l (loc_union (loc_union x r1) r2)) s))
  [SMTPat (loc_includes (loc_union l (loc_union (loc_union x r1) r2)) s)]
let loc_includes_union_assoc_focalize_2 l x r1 r2 s =
  loc_includes_trans (loc_union l (loc_union (loc_union x r1) r2)) (loc_union l (loc_union x (loc_union r1 r2))) s
val loc_includes_union_assoc_focalize_2
  (l x r1 r2 s: loc)
: Lemma
  (requires (loc_includes (loc_union l (loc_union x (loc_union r1 r2))) s))
  (ensures (loc_includes (loc_union l (loc_union (loc_union x r1) r2)) s))
  [SMTPat (loc_includes (loc_union l (loc_union (loc_union x r1) r2)) s)]
let loc_includes_union_assoc_focalize_2 l x r1 r2 s =
loc_includes_trans (loc_union l (loc_union (loc_union x r1) r2))
  (loc_union l (loc_union x (loc_union r1 r2)))
  s
FStar.Pointer.Derived1.fst.checked
prims.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
FStar.Pointer.Derived1.fst
FStar.Pointer.Base.loc FStar.Pointer.Base.loc_includes_trans FStar.Pointer.Base.loc_union Prims.unit
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Pointer.Derived1

module HH = FStar.HyperStack
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

let includes_gfield_gen #t p #l q fd =
  includes_gfield q fd;
  includes_trans p q (gfield q fd)

let includes_gufield_gen #t p #l q fd =
  includes_gufield q fd;
  includes_trans p q (gufield q fd)

let includes_gcell_gen #t p #length #value q i =
  includes_gcell q i;
  includes_trans p q (gcell q i)

let loc_includes_union_assoc_r2l s1 s2 s3 s =
  loc_includes_trans (loc_union (loc_union s1 s2) s3) (loc_union s1 (loc_union s2 s3)) s

let loc_includes_union_assoc_l2r s1 s2 s3 s =
  loc_includes_trans (loc_union s1 (loc_union s2 s3)) (loc_union (loc_union s1 s2) s3) s

let loc_includes_union_assoc_focalize_1 l1 l2 x r s =
  loc_includes_trans (loc_union l1 (loc_union (loc_union l2 x) r)) (loc_union (loc_union l1 l2) (loc_union x r)) s
val loc_includes_union_assoc_focalize_2
  (l x r1 r2 s: loc)
: Lemma
  (requires (loc_includes (loc_union l (loc_union x (loc_union r1 r2))) s))
  (ensures (loc_includes (loc_union l (loc_union (loc_union x r1) r2)) s))
  [SMTPat (loc_includes (loc_union l (loc_union (loc_union x r1) r2)) s)]

    l: FStar.Pointer.Base.loc ->
    x: FStar.Pointer.Base.loc ->
    r1: FStar.Pointer.Base.loc ->
    r2: FStar.Pointer.Base.loc ->
    s: FStar.Pointer.Base.loc
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Pointer.Base.loc_includes (FStar.Pointer.Base.loc_union l
              (FStar.Pointer.Base.loc_union x (FStar.Pointer.Base.loc_union r1 r2)))
          s)
      (ensures
        FStar.Pointer.Base.loc_includes (FStar.Pointer.Base.loc_union l
              (FStar.Pointer.Base.loc_union (FStar.Pointer.Base.loc_union x r1) r2))
          s)
      [
        SMTPat (FStar.Pointer.Base.loc_includes (FStar.Pointer.Base.loc_union l
                  (FStar.Pointer.Base.loc_union (FStar.Pointer.Base.loc_union x r1) r2))
              s)
      ]