val action_among_successors
      (sem: semantics_t)
      (action: sem.action_t)
      (successors: list (successor_info_t sem))
    : GTot ubool
val action_among_successors
      (sem: semantics_t)
      (action: sem.action_t)
      (successors: list (successor_info_t sem))
    : GTot ubool
let action_among_successors
  (sem: semantics_t)
  (action: sem.action_t)
  (successors: list (successor_info_t sem))
  : GTot ubool =
  exists successor. contains_ubool successor successors /\ successor.action == action
module Strategies.RegularToAtomic

open Armada.Action
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Transition
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.Atomic
open Strategies.Semantics
open Util.List
open Util.Nth

noeq type successor_info_t (sem: semantics_t) = {
  action: sem.action_t;
  path_index: nat;
}

noeq type atomic_path_info_t (sem: semantics_t) = {
  path: list sem.action_t;
  breaking: bool;
  // For a path that terminates in a break state, the index of the atomic action corresponding to it:
  atomic_action_index: nat;
  // For a path that doesn't terminate in a break state, the successor info for all the atomic paths that succeed it.
  successors: list (successor_info_t sem);
}
/
Util.Nth.fst.checked Util.List.fst.checked Strategies.Semantics.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 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.RegularToAtomic.fsti

    sem: Strategies.Semantics.semantics_t ->
    action: Mksemantics_t?.action_t sem ->
    successors: Prims.list (Strategies.RegularToAtomic.successor_info_t sem)
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Semantics.semantics_t Strategies.Semantics.__proj__Mksemantics_t__item__action_t Prims.list Strategies.RegularToAtomic.successor_info_t Prims.l_Exists Prims.l_and Spec.List.contains_ubool Prims.eq2 Strategies.RegularToAtomic.__proj__Mksuccessor_info_t__item__action Spec.Ubool.ubool
let action_among_successors
      (sem: semantics_t)
      (action: sem.action_t)
      (successors: list (successor_info_t sem))
    : GTot ubool =
  
exists successor. contains_ubool successor successors /\ successor.action == action