val var_intro_lh_relation (vr: var_intro_relation_t) (u: unit) (ls hs: Armada.State.t) : GTot ubool
val var_intro_lh_relation (vr: var_intro_relation_t) (u: unit) (ls hs: Armada.State.t) : GTot ubool
let var_intro_lh_relation
  (vr: var_intro_relation_t)
  (u: unit)
  (ls: Armada.State.t)
  (hs: Armada.State.t)
  : GTot ubool =
    var_intro_lh_relation_between_steps vr u ls hs
  /\ all_threads_breaking vr.is_breaking_hpc hs
module Strategies.VarIntro.Invariant

open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open Spec.List
open Spec.Ubool
open Strategies.ArmadaStatement.Breaking
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.ArmadaStatement.Status
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.GlobalVars
open Strategies.GlobalVars.Types
open Strategies.Invariant
open Strategies.PCRelation
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarIntro.Defs
open Strategies.VarIntro.Helpers
open Strategies.VarIntro.Initialization

let var_intro_invariant
  (ls: Armada.State.t)
  : GTot ubool =
  True

let var_intro_lh_relation_between_steps
  (vr: var_intro_relation_t)
  (u: unit)
  (ls: Armada.State.t)
  (hs: Armada.State.t)
  : GTot ubool =
  let pc_relation = var_intro_pc_relation vr.hpc_to_lpc vr.return_hpcs vr.return_pcs_unique_proof in
    states_match_except_global_variables vr.vs pc_relation ls hs
  /\ all_running_threads_have_pcs_in_list vr.hpcs hs
  /\ global_variables_unaddressed_in_memory vr.vs ls.mem
  /\ global_variables_unaddressed_in_memory vr.vs hs.mem
  /\ roots_match ls.mem
  /\ roots_match hs.mem
  /\ all_gvars_have_types hs.mem vr.vs vr.tds
  /\ unstarted_threads_have_empty_write_buffers ls
  /\ unstarted_threads_have_empty_write_buffers hs
  /\ (NotStopped? hs.stop_reason ==> vr.inv hs)
/
Strategies.VarIntro.Initialization.fsti.checked Strategies.VarIntro.Helpers.fst.checked Strategies.VarIntro.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCRelation.fst.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Strategies.ArmadaStatement.Status.fsti.checked Strategies.ArmadaStatement.Breaking.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.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Step.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.VarIntro.Invariant.fst

    vr: Strategies.VarIntro.Defs.var_intro_relation_t ->
    u19: Prims.unit ->
    ls: Armada.State.t ->
    hs: Armada.State.t
  -> Prims.GTot Spec.Ubool.ubool
Strategies.VarIntro.Defs.var_intro_relation_t Prims.unit Armada.State.t Prims.l_and Strategies.VarIntro.Invariant.var_intro_lh_relation_between_steps Strategies.ArmadaStatement.Breaking.all_threads_breaking Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__is_breaking_hpc Spec.Ubool.ubool
let var_intro_lh_relation (vr: var_intro_relation_t) (u: unit) (ls hs: Armada.State.t) : GTot ubool =
  
var_intro_lh_relation_between_steps vr u ls hs /\ all_threads_breaking vr.is_breaking_hpc hs