val action_pred (action: Armada.Action.t) : GTot ubool
val action_pred (action: Armada.Action.t) : GTot ubool
let action_pred (action: Armada.Action.t) : GTot ubool =
  True
module MyAtomicBInvariant

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.GlobalVars.Types
open Strategies.Invariant
open Strategies.Invariant.Armada
open Strategies.Invariant.Armada.AtomicSubstep
open Strategies.Semantics
open Strategies.Semantics.Armada
open Spec.List
open Spec.Ubool
open Util.List

let inv (s: Armada.State.t) : GTot ubool =
    gvar_has_type s.mem "a" (ObjectTDAbstract int)
  /\ gvar_has_type s.mem "c" (ObjectTDAbstract int)
  /\ gvar_has_type s.mem "e" (ObjectTDAbstract int)
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.AtomicSubstep.fsti.checked Strategies.Invariant.Armada.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.Types.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyAtomicBProg.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
MyAtomicBInvariant.fst
action: Armada.Action.t -> Prims.GTot Spec.Ubool.ubool
Armada.Action.t Prims.l_True Spec.Ubool.ubool
let action_pred (action: Armada.Action.t) : GTot ubool =
  
True