val my_atomic_to_regular_map:(list (list nat))
val my_atomic_to_regular_map:(list (list nat))
let my_atomic_to_regular_map: (list (list nat)) =
  [[0]; [1]; [2; 4; 6]; [3]; [2; 5]; [2; 4; 7]; [8]; [9]]
module MyAtomicToRegularRefinement

open Armada.Action
open Armada.BinaryOp
open Armada.Expression
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Type
open FStar.Tactics.V2
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.AtomicToRegular.Armada
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.Nth
/
Util.Nth.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.AtomicToRegular.Armada.fsti.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyHProg.fst.checked MyAtomicHProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Expression.fst.checked Armada.BinaryOp.fst.checked Armada.Action.fst.checked
MyAtomicToRegularRefinement.fst
Prims.list (Prims.list Prims.nat)
Prims.Cons Prims.list Prims.nat Prims.Nil
let my_atomic_to_regular_map:(list (list nat)) =
  
[[0]; [1]; [2; 4; 6]; [3]; [2; 5]; [2; 4; 7]; [8]; [9]]