val remove_hidden_initializers_ensures_memories_match_except_gvars
      (vs: list var_id_t)
      (which_are_hidings: list bool)
      (linits hinits: list initializer_t)
      (lmem: Armada.Memory.t)
    : Lemma (requires initializers_match_except_global_variables vs which_are_hidings linits hinits)
      (ensures
        (let hmem = remove_hidden_initializers which_are_hidings linits lmem in
          memories_match_except_global_variables vs lmem hmem))
val remove_hidden_initializers_ensures_memories_match_except_gvars
      (vs: list var_id_t)
      (which_are_hidings: list bool)
      (linits hinits: list initializer_t)
      (lmem: Armada.Memory.t)
    : Lemma (requires initializers_match_except_global_variables vs which_are_hidings linits hinits)
      (ensures
        (let hmem = remove_hidden_initializers which_are_hidings linits lmem in
          memories_match_except_global_variables vs lmem hmem))
let rec remove_hidden_initializers_ensures_memories_match_except_gvars
  (vs: list var_id_t)
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  : Lemma (requires initializers_match_except_global_variables vs which_are_hidings linits hinits)
          (ensures  (let hmem = remove_hidden_initializers which_are_hidings linits lmem in
                     memories_match_except_global_variables vs lmem hmem)) =
  match which_are_hidings, linits, hinits with
  | [], [], [] -> ()
  | true :: remaining_which_are_hidings, first_linit :: remaining_linits, _ ->
      remove_hidden_initializers_ensures_memories_match_except_gvars vs remaining_which_are_hidings remaining_linits
        hinits lmem
  | false :: remaining_which_are_hidings, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      remove_hidden_initializers_ensures_memories_match_except_gvars vs remaining_which_are_hidings remaining_linits
        remaining_hinits lmem
  | _, _, _ -> ()
module Strategies.VarHiding.Initialization

open Armada.Base
open Armada.Computation
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Type
open Spec.List
open Spec.Ubool
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.GlobalVars
open Strategies.GlobalVars.Init
open Strategies.GlobalVars.Permanent
open Strategies.GlobalVars.Statement
open Strategies.GlobalVars.Unaddressed
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.VarHiding
open Strategies.GlobalVars.VarIntro
open Strategies.Lift.Generic
open Strategies.Invariant
open Strategies.VarHiding.Defs
open Util.List
/
Util.List.fst.checked Strategies.VarHiding.Defs.fst.checked Strategies.Lift.Generic.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.VarHiding.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Statement.fsti.checked Strategies.GlobalVars.Permanent.fst.checked Strategies.GlobalVars.Init.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.UnstartedThreads.fsti.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked
Strategies.VarHiding.Initialization.fst

    vs: Prims.list Armada.Base.var_id_t ->
    which_are_hidings: Prims.list Prims.bool ->
    linits: Prims.list Armada.Init.initializer_t ->
    hinits: Prims.list Armada.Init.initializer_t ->
    lmem: Armada.Memory.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarHiding.Defs.initializers_match_except_global_variables vs
          which_are_hidings
          linits
          hinits)
      (ensures
        (let hmem =
            Strategies.VarHiding.Initialization.remove_hidden_initializers which_are_hidings
              linits
              lmem
          in
          Strategies.GlobalVars.memories_match_except_global_variables vs lmem hmem))
Prims.list Armada.Base.var_id_t Prims.bool Armada.Init.initializer_t Armada.Memory.t FStar.Pervasives.Native.Mktuple3 Strategies.VarHiding.Initialization.remove_hidden_initializers_ensures_memories_match_except_gvars Prims.unit Strategies.VarHiding.Defs.initializers_match_except_global_variables Prims.squash Strategies.GlobalVars.memories_match_except_global_variables Strategies.VarHiding.Initialization.remove_hidden_initializers Prims.Nil FStar.Pervasives.pattern
let rec remove_hidden_initializers_ensures_memories_match_except_gvars
      (vs: list var_id_t)
      (which_are_hidings: list bool)
      (linits hinits: list initializer_t)
      (lmem: Armada.Memory.t)
    : Lemma (requires initializers_match_except_global_variables vs which_are_hidings linits hinits)
      (ensures
        (let hmem = remove_hidden_initializers which_are_hidings linits lmem in
          memories_match_except_global_variables vs lmem hmem)) =
  
match which_are_hidings, linits, hinits with
| [], [], [] -> ()
| true :: remaining_which_are_hidings, first_linit :: remaining_linits, _ ->
  remove_hidden_initializers_ensures_memories_match_except_gvars vs
    remaining_which_are_hidings
    remaining_linits
    hinits
    lmem
| false :: remaining_which_are_hidings,
first_linit :: remaining_linits,
first_hinit :: remaining_hinits ->
  remove_hidden_initializers_ensures_memories_match_except_gvars vs
    remaining_which_are_hidings
    remaining_linits
    remaining_hinits
    lmem
| _, _, _ -> ()