val var_intro_witness_valid
      (latomic_prog hatomic_prog: program_t (make_atomic_semantics armada_semantics))
      (vw: var_intro_witness_t)
    : GTot ubool
val var_intro_witness_valid
      (latomic_prog hatomic_prog: program_t (make_atomic_semantics armada_semantics))
      (vw: var_intro_witness_t)
    : GTot ubool
let var_intro_witness_valid
  (latomic_prog: program_t (make_atomic_semantics armada_semantics))
  (hatomic_prog: program_t (make_atomic_semantics armada_semantics))
  (vw: var_intro_witness_t)
  : GTot ubool =
    program_inits_match_except_global_variables vw.vs vw.hpc_to_lpc vw.which_initializers_are_intros
      vw.lprog vw.hprog
  /\ vw.is_breaking_hpc vw.hprog.main_start_pc
  /\ initializers_with_same_variable_id_match vw.hprog.global_initializers
  /\ list_contains vw.hprog.main_start_pc vw.hpcs
  /\ vw.hpc_to_lpc vw.hprog.main_start_pc = vw.lprog.main_start_pc
  /\ global_variables_unaddressed_in_initializers vw.vs vw.lprog.global_initializers
  /\ global_variables_unaddressed_in_initializers vw.vs vw.hprog.global_initializers
  /\ global_variables_unaddressed_in_initializers vw.vs vw.lprog.main_stack_initializers
  /\ global_variables_unaddressed_in_initializers vw.vs vw.hprog.main_stack_initializers
  /\ every_variable_appears_among_initializers vw.hprog.global_initializers vw.vs vw.tds
  /\ for_all_ghost (for_all_ghost (pcs_contain_new_pcs_of_action vw.hpcs)) hatomic_prog.actions
  /\ every_hpc_appears_among_lpc_to_hpcs vw.lpc_to_hpcs vw.hpc_to_lpc vw.hpcs
  /\ return_pcs_unique vw.hpc_to_lpc vw.return_hpcs
  /\ each_action_list_consistent_with_is_nonyielding_pc vw.is_nonyielding_lpc latomic_prog.actions
  /\ each_action_list_consistent_with_is_nonyielding_pc vw.is_nonyielding_hpc hatomic_prog.actions
  /\ each_action_list_maintains_all_threads_breaking vw.is_breaking_hpc hatomic_prog.actions
  /\ each_action_list_doesnt_internally_yield latomic_prog.actions
  /\ each_action_list_doesnt_internally_yield hatomic_prog.actions
  /\ for_all_ubool (introduced_atomic_action_makes_progress vw.vs vw.tds vw.inv hatomic_prog.actions
                      vw.hpc_info vw.hpc_to_lpc vw.is_nonyielding_lpc) vw.hpcs
  /\ lists_correspond_ubool
       (lactions_correspond_to_hactions_per_correspondence vw.vs vw.tds vw.inv
          vw.hpc_to_lpc vw.lpc_to_hpcs vw.return_hpcs vw.is_breaking_hpc vw.hpc_info hatomic_prog.actions)
      latomic_prog.actions vw.corresponding_hactions_info
module Strategies.VarIntro.Inefficient

open Armada.Action
open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Threads
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.Breaking
open Strategies.GlobalVars
open Strategies.GlobalVars.Permanent
open Strategies.GlobalVars.Statement
open Strategies.GlobalVars.VarIntro
open Strategies.Invariant
open Strategies.Invariant.Armada.AtomicSubstep
open Strategies.Nonyielding
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarIntro.Defs
open Util.List
open Util.Nth
open Util.Relation

noeq type var_intro_witness_t = {
  lprog: Armada.Program.t;
  hprog: Armada.Program.t;
  vs: list var_id_t;
  tds: list object_td_t;
  inv: invariant_t Armada.State.t;
  which_initializers_are_intros: list bool;
  hpc_to_lpc: pc_t -> GTot pc_t;
  lpc_to_hpcs: pc_t -> GTot (list pc_t);
  return_hpcs: list pc_t;
  is_nonyielding_lpc: pc_t -> GTot bool;
  is_nonyielding_hpc: pc_t -> GTot bool;
  is_breaking_hpc: pc_t -> GTot bool;
  hpcs: list pc_t;
  hpc_info: pc_t -> GTot (hpc_info_t vs tds inv);
  corresponding_hactions_info: list (ltoh_correspondence_t vs tds inv);
}
/
Util.Relation.fst.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.VarIntro.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Nonyielding.fst.checked Strategies.Invariant.Armada.AtomicSubstep.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.Statement.fsti.checked Strategies.GlobalVars.Permanent.fst.checked Strategies.GlobalVars.fst.checked Strategies.Breaking.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.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 Armada.Action.fst.checked
Strategies.VarIntro.Inefficient.fsti

    latomic_prog:
      Strategies.Semantics.program_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          ) ->
    hatomic_prog:
      Strategies.Semantics.program_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          ) ->
    vw: Strategies.VarIntro.Inefficient.var_intro_witness_t
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Semantics.program_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Strategies.VarIntro.Inefficient.var_intro_witness_t Prims.l_and Strategies.VarIntro.Defs.program_inits_match_except_global_variables Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__vs Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__hpc_to_lpc Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__which_initializers_are_intros Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__lprog Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__hprog Prims.b2t Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__is_breaking_hpc Armada.Program.__proj__Mkt__item__main_start_pc Strategies.VarIntro.Defs.initializers_with_same_variable_id_match Armada.Program.__proj__Mkt__item__global_initializers Spec.List.list_contains Armada.Base.pc_t Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__hpcs Prims.op_Equality Strategies.GlobalVars.global_variables_unaddressed_in_initializers Armada.Program.__proj__Mkt__item__main_stack_initializers Strategies.VarIntro.Defs.every_variable_appears_among_initializers Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__tds Util.List.for_all_ghost Strategies.Semantics.__proj__Mksemantics_t__item__action_t Armada.Action.t Strategies.VarIntro.Defs.pcs_contain_new_pcs_of_action Strategies.Semantics.__proj__Mkprogram_t__item__actions Strategies.VarIntro.Defs.every_hpc_appears_among_lpc_to_hpcs Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__lpc_to_hpcs Strategies.VarIntro.Defs.return_pcs_unique Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__return_hpcs Strategies.Nonyielding.each_action_list_consistent_with_is_nonyielding_pc Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__is_nonyielding_lpc Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__is_nonyielding_hpc Strategies.Breaking.each_action_list_maintains_all_threads_breaking Strategies.Nonyielding.each_action_list_doesnt_internally_yield Util.List.for_all_ubool Strategies.VarIntro.Defs.introduced_atomic_action_makes_progress Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__inv Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__hpc_info Util.List.lists_correspond_ubool Strategies.VarIntro.Defs.ltoh_correspondence_t Strategies.VarIntro.Defs.lactions_correspond_to_hactions_per_correspondence Strategies.VarIntro.Inefficient.__proj__Mkvar_intro_witness_t__item__corresponding_hactions_info Spec.Ubool.ubool
let var_intro_witness_valid
      (latomic_prog hatomic_prog: program_t (make_atomic_semantics armada_semantics))
      (vw: var_intro_witness_t)
    : GTot ubool =
  
program_inits_match_except_global_variables vw.vs
  vw.hpc_to_lpc
  vw.which_initializers_are_intros
  vw.lprog
  vw.hprog /\ vw.is_breaking_hpc vw.hprog.main_start_pc /\
initializers_with_same_variable_id_match vw.hprog.global_initializers /\
list_contains vw.hprog.main_start_pc vw.hpcs /\
vw.hpc_to_lpc vw.hprog.main_start_pc = vw.lprog.main_start_pc /\
global_variables_unaddressed_in_initializers vw.vs vw.lprog.global_initializers /\
global_variables_unaddressed_in_initializers vw.vs vw.hprog.global_initializers /\
global_variables_unaddressed_in_initializers vw.vs vw.lprog.main_stack_initializers /\
global_variables_unaddressed_in_initializers vw.vs vw.hprog.main_stack_initializers /\
every_variable_appears_among_initializers vw.hprog.global_initializers vw.vs vw.tds /\
for_all_ghost (for_all_ghost (pcs_contain_new_pcs_of_action vw.hpcs)) hatomic_prog.actions /\
every_hpc_appears_among_lpc_to_hpcs vw.lpc_to_hpcs vw.hpc_to_lpc vw.hpcs /\
return_pcs_unique vw.hpc_to_lpc vw.return_hpcs /\
each_action_list_consistent_with_is_nonyielding_pc vw.is_nonyielding_lpc latomic_prog.actions /\
each_action_list_consistent_with_is_nonyielding_pc vw.is_nonyielding_hpc hatomic_prog.actions /\
each_action_list_maintains_all_threads_breaking vw.is_breaking_hpc hatomic_prog.actions /\
each_action_list_doesnt_internally_yield latomic_prog.actions /\
each_action_list_doesnt_internally_yield hatomic_prog.actions /\
for_all_ubool (introduced_atomic_action_makes_progress vw.vs
      vw.tds
      vw.inv
      hatomic_prog.actions
      vw.hpc_info
      vw.hpc_to_lpc
      vw.is_nonyielding_lpc)
  vw.hpcs /\
lists_correspond_ubool (lactions_correspond_to_hactions_per_correspondence vw.vs
      vw.tds
      vw.inv
      vw.hpc_to_lpc
      vw.lpc_to_hpcs
      vw.return_hpcs
      vw.is_breaking_hpc
      vw.hpc_info
      hatomic_prog.actions)
  latomic_prog.actions
  vw.corresponding_hactions_info