val valid_atomic_to_regular_map
      (sem: semantics_t)
      (atomic_actions: list (list sem.action_t))
      (regular_actions: list sem.action_t)
      (atomic_to_regular_map: list (list nat))
    : GTot ubool
val valid_atomic_to_regular_map
      (sem: semantics_t)
      (atomic_actions: list (list sem.action_t))
      (regular_actions: list sem.action_t)
      (atomic_to_regular_map: list (list nat))
    : GTot ubool
let valid_atomic_to_regular_map
  (sem: semantics_t)
  (atomic_actions: list (list sem.action_t))
  (regular_actions: list sem.action_t)
  (atomic_to_regular_map: list (list nat))
  : GTot ubool =
  let index_and_action_corr = fun index -> fun action -> (nth regular_actions index) == (Some action) in
  let indices_and_actions_corr =
    fun indices -> fun atomic_action -> lists_correspond_ubool index_and_action_corr indices atomic_action in
  lists_correspond_ubool indices_and_actions_corr atomic_to_regular_map atomic_actions
module Strategies.AtomicToRegular

open Armada.Action
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Transition
open Spec.Behavior
open FStar.List.Tot
open Spec.Ubool
open Strategies.Atomic
open Strategies.Semantics
open Util.Behavior
open Util.List
open Util.Nth
/
Util.Nth.fst.checked Util.List.fst.checked Util.Behavior.fst.checked Strategies.Semantics.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Action.fst.checked
Strategies.AtomicToRegular.fsti

    sem: Strategies.Semantics.semantics_t ->
    atomic_actions: Prims.list (Prims.list (Mksemantics_t?.action_t sem)) ->
    regular_actions: Prims.list (Mksemantics_t?.action_t sem) ->
    atomic_to_regular_map: Prims.list (Prims.list Prims.nat)
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Semantics.semantics_t Prims.list Strategies.Semantics.__proj__Mksemantics_t__item__action_t Prims.nat Util.List.lists_correspond_ubool Spec.Ubool.ubool Prims.logical Prims.eq2 FStar.Pervasives.Native.option FStar.List.Tot.Base.nth FStar.Pervasives.Native.Some
let valid_atomic_to_regular_map
      (sem: semantics_t)
      (atomic_actions: list (list sem.action_t))
      (regular_actions: list sem.action_t)
      (atomic_to_regular_map: list (list nat))
    : GTot ubool =
  
let index_and_action_corr =
  fun index -> fun action -> (nth regular_actions index) == (Some action)
in
let indices_and_actions_corr =
  fun indices ->
    fun atomic_action -> lists_correspond_ubool index_and_action_corr indices atomic_action
in
lists_correspond_ubool indices_and_actions_corr atomic_to_regular_map atomic_actions