val my_lpcs:array_t pc_t
val my_lpcs:array_t pc_t
let my_lpcs: array_t pc_t = list_to_array [ "main.0"; "main.1"; "main.2"; "main.3"; "main.4"; "main.5" ]
module MyRegularToAtomicRefinement

open Armada.Action
open Armada.Base
open Armada.BinaryOp
open Armada.Expression
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open FStar.Tactics.V2
open MyAtomicLProg
open MyLProg
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.Atomic
open Strategies.PCIndices
open Strategies.RegularToAtomic
open Strategies.RegularToAtomic.Armada
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.Nth
open Util.Range

// This is all the PCs in the program.
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.Armada.fsti.checked Strategies.RegularToAtomic.fsti.checked Strategies.PCIndices.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.Logic.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.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Expression.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyRegularToAtomicRefinement.fst
Util.ImmutableArray.array_t Armada.Base.pc_t
Util.ImmutableArray.list_to_array Armada.Base.pc_t Prims.Cons Prims.Nil
let my_lpcs:array_t pc_t =
  
list_to_array ["main.0"; "main.1"; "main.2"; "main.3"; "main.4"; "main.5"]