val pointer_among_gvars_implies_gvars_addressed
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  : Lemma (requires pointer_among_global_variables vs p)
          (ensures  not (global_variables_unaddressed_in_pointer vs p))
val pointer_among_gvars_implies_gvars_addressed
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  : Lemma (requires pointer_among_global_variables vs p)
          (ensures  not (global_variables_unaddressed_in_pointer vs p))
let rec pointer_among_gvars_implies_gvars_addressed
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  : Lemma (requires pointer_among_global_variables vs p)
          (ensures  not (global_variables_unaddressed_in_pointer vs p)) =
  match p with
  | PointerUninitialized -> ()
  | PointerNull -> ()
  | PointerRoot root_id -> ()
  | PointerField struct_ptr _ -> pointer_among_gvars_implies_gvars_addressed vs struct_ptr
  | PointerIndex array_ptr _ -> pointer_among_gvars_implies_gvars_addressed vs array_ptr
module Strategies.GlobalVars.VarIntro

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.Util
open Strategies.PCRelation
open Util.Seq
open Util.Trigger
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Strategies.PCRelation.fst.checked Strategies.GlobalVars.Util.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.List.Tot.fst.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.VarIntro.fst
vs: Prims.list Armada.Base.var_id_t -> p: Armada.Pointer.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.GlobalVars.VarIntro.pointer_among_global_variables vs p)
      (ensures
        Prims.op_Negation (Strategies.GlobalVars.global_variables_unaddressed_in_pointer vs p))
Prims.list Armada.Base.var_id_t Armada.Pointer.t Armada.Base.root_id_t Prims.nat Strategies.GlobalVars.VarIntro.pointer_among_gvars_implies_gvars_addressed Prims.unit Prims.b2t Strategies.GlobalVars.VarIntro.pointer_among_global_variables Prims.squash Prims.op_Negation Strategies.GlobalVars.global_variables_unaddressed_in_pointer Prims.Nil FStar.Pervasives.pattern
let rec pointer_among_gvars_implies_gvars_addressed (vs: list var_id_t) (p: Armada.Pointer.t)
    : Lemma (requires pointer_among_global_variables vs p)
      (ensures not (global_variables_unaddressed_in_pointer vs p)) =
  
match p with
| PointerUninitialized -> ()
| PointerNull -> ()
| PointerRoot root_id -> ()
| PointerField struct_ptr _ -> pointer_among_gvars_implies_gvars_addressed vs struct_ptr
| PointerIndex array_ptr _ -> pointer_among_gvars_implies_gvars_addressed vs array_ptr