val var_intro_invariant (ls: Armada.State.t) : GTot ubool
val var_intro_invariant (ls: Armada.State.t) : GTot ubool
let var_intro_invariant
  (ls: Armada.State.t)
  : GTot ubool =
  True
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
/
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
ls: Armada.State.t -> Prims.GTot Spec.Ubool.ubool
Armada.State.t Prims.l_True Spec.Ubool.ubool
let var_intro_invariant (ls: Armada.State.t) : GTot ubool =
  
True