val my_action_pred (action: Armada.Action.t) : GTot ubool
val my_action_pred (action: Armada.Action.t) : GTot ubool
let my_action_pred (action: Armada.Action.t) : GTot ubool =
      (not action.ok)
    \/ (  global_variables_unmodifiable_by_statement vs action.program_statement.statement
       /\ global_variables_unaddressable_in_statement vs action.program_statement.statement)
module GlobalVarExampleInvariant

open Armada.Action
open Armada.Base
open Armada.BinaryOp
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open Spec.Behavior
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Invariant.Armada.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Spec.List
open Spec.Ubool
open Util.List

open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Init
open Strategies.GlobalVarsProof
open Strategies.GlobalVars.UnaddressedStatement

let vs = ["f"]

let my_inv (s: Armada.State.t) : GTot ubool =
  let root_one: root_t = RootGlobal (ObjectStorageAbstract int 1) in
    s.mem (RootIdGlobal "f") == root_one
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.Atomic.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVarsProof.fst.checked Strategies.GlobalVars.UnaddressedStatement.fst.checked Strategies.GlobalVars.Init.fst.checked Strategies.GlobalVars.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyLProg.fst.checked MyAtomicLProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
GlobalVarExampleInvariant.fst
action: Armada.Action.t -> Prims.GTot Spec.Ubool.ubool
Armada.Action.t Prims.l_or Prims.b2t Prims.op_Negation Armada.Action.__proj__Mkt__item__ok Prims.l_and Strategies.GlobalVars.global_variables_unmodifiable_by_statement GlobalVarExampleInvariant.vs Armada.Action.__proj__Mkprogram_statement_t__item__statement Armada.Action.__proj__Mkt__item__program_statement Strategies.GlobalVars.global_variables_unaddressable_in_statement Spec.Ubool.ubool
let my_action_pred (action: Armada.Action.t) : GTot ubool =
  
(not action.ok) \/
(global_variables_unmodifiable_by_statement vs action.program_statement.statement /\
  global_variables_unaddressable_in_statement vs action.program_statement.statement)