val memories_match_except_global_variables_transitive
      (vs: list var_id_t)
      (mem1 mem2 mem3: Armada.Memory.t)
    : Lemma
      (requires
        memories_match_except_global_variables vs mem1 mem2 /\
        memories_match_except_global_variables vs mem2 mem3)
      (ensures memories_match_except_global_variables vs mem1 mem3)
val memories_match_except_global_variables_transitive
      (vs: list var_id_t)
      (mem1 mem2 mem3: Armada.Memory.t)
    : Lemma
      (requires
        memories_match_except_global_variables vs mem1 mem2 /\
        memories_match_except_global_variables vs mem2 mem3)
      (ensures memories_match_except_global_variables vs mem1 mem3)
let memories_match_except_global_variables_transitive
  (vs: list var_id_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  (mem3: Armada.Memory.t)
  : Lemma (requires   memories_match_except_global_variables vs mem1 mem2
                    /\ memories_match_except_global_variables vs mem2 mem3)
          (ensures  memories_match_except_global_variables vs mem1 mem3) =
  introduce forall root_id. (match root_id with
                        | RootIdGlobal v -> list_contains v vs \/ (mem1 root_id == mem3 root_id)
                        | _ -> mem1 root_id == mem3 root_id)
  with (
    match root_id with
    | RootIdGlobal v ->
        assert (list_contains v vs \/ (mem1 root_id == mem2 root_id));
        assert (list_contains v vs \/ (mem2 root_id == mem3 root_id))
    | _ ->
        assert (mem1 root_id == mem2 root_id);
        assert (mem2 root_id == mem3 root_id)
  )
module Strategies.GlobalVars.Util

open Armada.Base
open Armada.BinaryOp
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open Armada.UnaryOp
open FStar.Sequence.Ambient
open FStar.Sequence.Base
open Spec.List
open Spec.Ubool
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Pointer
open Strategies.GlobalVars.Unaddressed
open Strategies.GlobalVars.Value
open Strategies.PCRelation
open Util.List
open Util.Nth
open Util.Seq
open Util.Trigger

let memories_match_except_global_variables_reflexive (vs: list var_id_t) (mem: Armada.Memory.t)
  : Lemma (memories_match_except_global_variables vs mem mem) =
  ()

let memories_match_except_global_variables_commutative
  (vs: list var_id_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (memories_match_except_global_variables vs mem1 mem2 <==>
             memories_match_except_global_variables vs mem2 mem1) =
  ()
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.PCRelation.fst.checked Strategies.GlobalVars.Value.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Pointer.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Sequence.Ambient.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.UnaryOp.fst.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked
Strategies.GlobalVars.Util.fst

    vs: Prims.list Armada.Base.var_id_t ->
    mem1: Armada.Memory.t ->
    mem2: Armada.Memory.t ->
    mem3: Armada.Memory.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.memories_match_except_global_variables vs mem1 mem2 /\
        Strategies.GlobalVars.memories_match_except_global_variables vs mem2 mem3)
      (ensures Strategies.GlobalVars.memories_match_except_global_variables vs mem1 mem3)
Prims.list Armada.Base.var_id_t Armada.Memory.t FStar.Classical.Sugar.forall_intro Armada.Base.root_id_t Prims.l_or Prims.b2t Spec.List.list_contains Prims.eq2 Armada.Memory.root_t Prims._assert Prims.unit Prims.squash Prims.l_and Strategies.GlobalVars.memories_match_except_global_variables Prims.Nil FStar.Pervasives.pattern
let memories_match_except_global_variables_transitive
      (vs: list var_id_t)
      (mem1 mem2 mem3: Armada.Memory.t)
    : Lemma
      (requires
        memories_match_except_global_variables vs mem1 mem2 /\
        memories_match_except_global_variables vs mem2 mem3)
      (ensures memories_match_except_global_variables vs mem1 mem3) =
  
introduce forall root_id . (match root_id with
  | RootIdGlobal v -> list_contains v vs \/ (mem1 root_id == mem3 root_id)
  | _ -> mem1 root_id == mem3 root_id)
with (match root_id with
  | RootIdGlobal v ->
    assert (list_contains v vs \/ (mem1 root_id == mem2 root_id));
    assert (list_contains v vs \/ (mem2 root_id == mem3 root_id))
  | _ ->
    assert (mem1 root_id == mem2 root_id);
    assert (mem2 root_id == mem3 root_id))