val all_variables_among_gvars (mem: Armada.Memory.t) (vs: list var_id_t) : GTot bool
val all_variables_among_gvars (mem: Armada.Memory.t) (vs: list var_id_t) : GTot bool
let all_variables_among_gvars (mem: Armada.Memory.t) (vs: list var_id_t) : GTot bool =
  for_all_ghost (variable_among_gvars mem) vs
module Strategies.GlobalVars.Permanent

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open FStar.Tactics.V2
open Spec.List
open Spec.Map
open Spec.Ubool
open Strategies.ArmadaStatement
open Util.List
open Util.Tactics

let variable_among_gvars (mem: Armada.Memory.t) (v: var_id_t) : GTot bool =
  let root_id = RootIdGlobal v in
  let root = mem root_id in
  RootGlobal? root
/
Util.Tactics.fst.checked Util.List.fst.checked Strategies.ArmadaStatement.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.GlobalVars.Permanent.fst
mem: Armada.Memory.t -> vs: Prims.list Armada.Base.var_id_t -> Prims.GTot Prims.bool
Armada.Memory.t Prims.list Armada.Base.var_id_t Util.List.for_all_ghost Strategies.GlobalVars.Permanent.variable_among_gvars Prims.bool
let all_variables_among_gvars (mem: Armada.Memory.t) (vs: list var_id_t) : GTot bool =
  
for_all_ghost (variable_among_gvars mem) vs