val my_special_case_action_1:list Armada.Action.t
val my_special_case_action_1:list Armada.Action.t
let my_special_case_action_1 : list Armada.Action.t =
  [ { ok = false;
      program_statement = { start_pc = Some "main.0"; end_pc = Some "main.1"; starts_atomic_block = true;
                            ends_atomic_block = true;
                            statement = UpdateStatement false (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                          (ExpressionGlobalVariable (ObjectTDAbstract int) "f"); } } ]
module MyProgramProof

open Armada.Action
open Armada.Base
open Armada.Expression
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Transition
open Armada.Type
open FStar.List.Tot.Base
open FStar.Tactics.V2
open MyAtomicToRegularRefinement
open MyProgramInvariant
open MyRegularToAtomicRefinement
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Invariant.Armada.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.Weakening.Armada
open Util.Behavior
open Util.ImmutableArray
open Util.List

private let my_special_case_action_0 : list Armada.Action.t =
  [ { ok = true;
      program_statement = { start_pc = Some "main.0"; end_pc = Some "main.1"; starts_atomic_block = true;
                            ends_atomic_block = true;
                            statement = UpdateStatement false (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                          (ExpressionGlobalVariable (ObjectTDAbstract int) "f"); } } ]
/
Util.List.fst.checked Util.ImmutableArray.fsti.checked Util.Behavior.fst.checked Strategies.Weakening.Armada.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.Atomic.fsti.checked Strategies.Invariant.fsti.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyRegularToAtomicRefinement.fst.checked MyProgramInvariant.fst.checked MyLProg.fst.checked MyHProg.fst.checked MyAtomicToRegularRefinement.fst.checked MyAtomicLProg.fst.checked MyAtomicHProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.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.Expression.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyProgramProof.fst
Prims.list Armada.Action.t
Prims.Cons Armada.Action.t Armada.Action.Mkt Armada.Action.Mkprogram_statement_t FStar.Pervasives.Native.Some Armada.Base.pc_t Armada.Statement.UpdateStatement Armada.Expression.ExpressionGlobalVariable Armada.Type.ObjectTDAbstract Prims.int Prims.Nil
let my_special_case_action_1:list Armada.Action.t =
  
[
  {
    ok = false;
    program_statement
    =
    {
      start_pc = Some "main.0";
      end_pc = Some "main.1";
      starts_atomic_block = true;
      ends_atomic_block = true;
      statement
      =
      UpdateStatement false
        (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
        (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
    }
  }
]