val steps_then_steps_computation
      (sem: semantics_t)
      (actor: sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (steps1 steps2: list sem.step_t)
      (s: sem.state_t)
    : GTot (option sem.state_t)
val steps_then_steps_computation
      (sem: semantics_t)
      (actor: sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (steps1 steps2: list sem.step_t)
      (s: sem.state_t)
    : GTot (option sem.state_t)
let steps_then_steps_computation
  (sem: semantics_t)
  (actor: sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (steps1: list sem.step_t)
  (steps2: list sem.step_t)
  (s: sem.state_t)
  : GTot (option sem.state_t) =
  match steps_computation_generic sem actor starts_atomic_block false steps1 s with
  | None -> None
  | Some s' -> steps_computation_generic sem actor false ends_atomic_block steps2 s'
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.List
open Spec.Ubool
open Strategies.Atomic
open Util.Behavior
open Util.List
open Util.Nth
/
Util.Nth.fst.checked Util.List.fst.checked Util.Behavior.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.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.fst

    sem: Strategies.Semantics.semantics_t ->
    actor: Mksemantics_t?.actor_t sem ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    steps1: Prims.list (Mksemantics_t?.step_t sem) ->
    steps2: Prims.list (Mksemantics_t?.step_t sem) ->
    s: Mksemantics_t?.state_t sem
  -> Prims.GTot (FStar.Pervasives.Native.option (Mksemantics_t?.state_t sem))
Strategies.Semantics.semantics_t Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Prims.bool Prims.list Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Semantics.steps_computation_generic FStar.Pervasives.Native.None FStar.Pervasives.Native.option
let steps_then_steps_computation
      (sem: semantics_t)
      (actor: sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (steps1 steps2: list sem.step_t)
      (s: sem.state_t)
    : GTot (option sem.state_t) =
  
match steps_computation_generic sem actor starts_atomic_block false steps1 s with
| None -> None
| Some s' -> steps_computation_generic sem actor false ends_atomic_block steps2 s'