val memory_satisfies_main_stack_initializers_implies_satisfies_initializer
      (mem: Armada.Memory.t)
      (tid: tid_t)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (var_ids: list var_id_t)
      (initializers: list initializer_t)
      (initializer: initializer_t)
    : Lemma
      (requires
        contains_ubool initializer initializers /\
        memory_satisfies_main_stack_initializers mem tid method_id frame_uniq var_ids initializers)
      (ensures
        memory_satisfies_main_stack_initializer mem
          tid
          method_id
          frame_uniq
          initializer.var_id
          initializer)
val memory_satisfies_main_stack_initializers_implies_satisfies_initializer
      (mem: Armada.Memory.t)
      (tid: tid_t)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (var_ids: list var_id_t)
      (initializers: list initializer_t)
      (initializer: initializer_t)
    : Lemma
      (requires
        contains_ubool initializer initializers /\
        memory_satisfies_main_stack_initializers mem tid method_id frame_uniq var_ids initializers)
      (ensures
        memory_satisfies_main_stack_initializer mem
          tid
          method_id
          frame_uniq
          initializer.var_id
          initializer)
let rec memory_satisfies_main_stack_initializers_implies_satisfies_initializer
  (mem: Armada.Memory.t)
  (tid: tid_t)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (var_ids: list var_id_t)
  (initializers: list initializer_t)
  (initializer: initializer_t)
  : Lemma (requires   contains_ubool initializer initializers
                    /\ memory_satisfies_main_stack_initializers mem tid method_id frame_uniq var_ids initializers)
          (ensures  memory_satisfies_main_stack_initializer mem tid method_id frame_uniq initializer.var_id
                      initializer) =
  match var_ids, initializers with
  | first_var_id :: remaining_var_ids, first_initializer :: remaining_initializers ->
      if eqb first_initializer initializer then
        ()
      else
        memory_satisfies_main_stack_initializers_implies_satisfies_initializer mem tid method_id frame_uniq
          remaining_var_ids remaining_initializers initializer
module Strategies.GlobalVars.Init

open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open Spec.List
open Spec.Ubool
open Strategies.GlobalVars
open Strategies.GlobalVars.Util
open Util.List
/
Util.List.fst.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.fst.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.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Base.fst.checked
Strategies.GlobalVars.Init.fst

    mem: Armada.Memory.t ->
    tid: Armada.Base.tid_t ->
    method_id: Armada.Base.method_id_t ->
    frame_uniq: Armada.Base.root_id_uniquifier_t ->
    var_ids: Prims.list Armada.Base.var_id_t ->
    initializers: Prims.list Armada.Init.initializer_t ->
    initializer: Armada.Init.initializer_t
  -> FStar.Pervasives.Lemma
      (requires
        Spec.List.contains_ubool initializer initializers /\
        Armada.Init.memory_satisfies_main_stack_initializers mem
          tid
          method_id
          frame_uniq
          var_ids
          initializers)
      (ensures
        Armada.Init.memory_satisfies_main_stack_initializer mem
          tid
          method_id
          frame_uniq
          (Mkinitializer_t?.var_id initializer)
          initializer)
Armada.Memory.t Armada.Base.tid_t Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Prims.list Armada.Base.var_id_t Armada.Init.initializer_t FStar.Pervasives.Native.Mktuple2 Spec.Ubool.eqb Prims.bool Strategies.GlobalVars.Init.memory_satisfies_main_stack_initializers_implies_satisfies_initializer Prims.unit Prims.l_and Spec.List.contains_ubool Prims.b2t Armada.Init.memory_satisfies_main_stack_initializers Prims.squash Armada.Init.memory_satisfies_main_stack_initializer Armada.Init.__proj__Mkinitializer_t__item__var_id Prims.Nil FStar.Pervasives.pattern
let rec memory_satisfies_main_stack_initializers_implies_satisfies_initializer
      (mem: Armada.Memory.t)
      (tid: tid_t)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (var_ids: list var_id_t)
      (initializers: list initializer_t)
      (initializer: initializer_t)
    : Lemma
      (requires
        contains_ubool initializer initializers /\
        memory_satisfies_main_stack_initializers mem tid method_id frame_uniq var_ids initializers)
      (ensures
        memory_satisfies_main_stack_initializer mem
          tid
          method_id
          frame_uniq
          initializer.var_id
          initializer) =
  
match var_ids, initializers with
| first_var_id :: remaining_var_ids, first_initializer :: remaining_initializers ->
  if eqb first_initializer initializer
  then ()
  else
    memory_satisfies_main_stack_initializers_implies_satisfies_initializer mem
      tid
      method_id
      frame_uniq
      remaining_var_ids
      remaining_initializers
      initializer