val path_successor_matches_path_info
      (atomic_path_infos: list (atomic_path_info_t armada_semantics))
      (atomic_path_info: atomic_path_info_t armada_semantics)
      (successor: successor_info_t armada_semantics)
    : GTot ubool
val path_successor_matches_path_info
      (atomic_path_infos: list (atomic_path_info_t armada_semantics))
      (atomic_path_info: atomic_path_info_t armada_semantics)
      (successor: successor_info_t armada_semantics)
    : GTot ubool
let path_successor_matches_path_info
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  (atomic_path_info: atomic_path_info_t armada_semantics)
  (successor: successor_info_t armada_semantics)
  : GTot ubool =
     successor.path_index < length atomic_path_infos
  /\ (index atomic_path_infos successor.path_index).path == append atomic_path_info.path [successor.action]
module Strategies.RegularToAtomic.Armada.Helper

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Map
open Spec.Ubool
open Strategies.ArmadaStatement.Status
open Strategies.Atomic
open Strategies.RegularToAtomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.Behavior
open Util.List
open Util.Nth

let is_breaking_optional_pc
  (pc_breaking: pc_t -> GTot bool)
  (optional_pc: option pc_t)
  : GTot bool =
  match optional_pc with
  | Some pc -> pc_breaking pc
  | None -> true

let pc_breaking_correct_specific
  (pc_breaking: pc_t -> GTot bool)
  (ps: program_statement_t)
  : GTot bool =
     is_breaking_optional_pc pc_breaking ps.start_pc = ps.starts_atomic_block
  && is_breaking_optional_pc pc_breaking ps.end_pc = ps.ends_atomic_block
  && (implies (None? ps.end_pc) (is_breaking_optional_pc pc_breaking ps.start_pc))

let pc_breaking_correct
  (lprog: Armada.Program.t)
  (pc_breaking: pc_t -> GTot bool)
  : GTot bool =
  for_all_ghost (pc_breaking_correct_specific pc_breaking) lprog.program_statements

let created_threads_initially_breaking_specific
  (pc_breaking: pc_t -> GTot bool)
  (ps: program_statement_t)
  : GTot bool =
  match ps.statement with
  | CreateThreadStatement _ initial_pc _ _ _ _ _ -> pc_breaking initial_pc
  | _ -> true

let created_threads_initially_breaking
  (lprog: Armada.Program.t)
  (pc_breaking: pc_t -> GTot bool)
  : GTot bool =
  for_all_ghost (created_threads_initially_breaking_specific pc_breaking) lprog.program_statements

let actions_starting_at_pc_correct_specific
  (actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t))
  (action: Armada.Action.t)
  : GTot ubool =
  contains_ubool action (actions_starting_at_pc action.program_statement.start_pc)

let actions_starting_at_pc_correct
  (lprog: Armada.Program.t)
  (actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t))
  : GTot ubool =
  for_all_ubool (actions_starting_at_pc_correct_specific actions_starting_at_pc) (all_actions lprog.program_statements)

let starting_successors_match_path_infos_specific
  (starting_successors: list (successor_info_t armada_semantics))
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  (successor: successor_info_t armada_semantics)
  : GTot ubool =
    successor.path_index < length atomic_path_infos
  /\ (index atomic_path_infos successor.path_index).path == [successor.action]

let starting_successors_match_path_infos
  (starting_successors: list (successor_info_t armada_semantics))
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool
    (starting_successors_match_path_infos_specific starting_successors atomic_path_infos)
    starting_successors
/
Util.Nth.fst.checked Util.List.fst.checked Util.Behavior.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.fsti.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.Status.fsti.checked Spec.Ubool.fst.checked Spec.Map.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.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.RegularToAtomic.Armada.Helper.fst

    atomic_path_infos:
      Prims.list (Strategies.RegularToAtomic.atomic_path_info_t Strategies.Semantics.Armada.armada_semantics
          ) ->
    atomic_path_info:
      Strategies.RegularToAtomic.atomic_path_info_t Strategies.Semantics.Armada.armada_semantics ->
    successor:
      Strategies.RegularToAtomic.successor_info_t Strategies.Semantics.Armada.armada_semantics
  -> Prims.GTot Spec.Ubool.ubool
Prims.list Strategies.RegularToAtomic.atomic_path_info_t Strategies.Semantics.Armada.armada_semantics Strategies.RegularToAtomic.successor_info_t Prims.l_and Prims.b2t Prims.op_LessThan Strategies.RegularToAtomic.__proj__Mksuccessor_info_t__item__path_index FStar.List.Tot.Base.length Prims.eq2 Strategies.Semantics.__proj__Mksemantics_t__item__action_t Strategies.RegularToAtomic.__proj__Mkatomic_path_info_t__item__path FStar.List.Tot.Base.index FStar.List.Tot.Base.append Prims.Cons Strategies.RegularToAtomic.__proj__Mksuccessor_info_t__item__action Prims.Nil Spec.Ubool.ubool
let path_successor_matches_path_info
      (atomic_path_infos: list (atomic_path_info_t armada_semantics))
      (atomic_path_info: atomic_path_info_t armada_semantics)
      (successor: successor_info_t armada_semantics)
    : GTot ubool =
  
successor.path_index < length atomic_path_infos /\
(index atomic_path_infos successor.path_index).path ==
append atomic_path_info.path [successor.action]