val armada_actions_starting_at_pc_correct
      (action_indices_starting_at_no_pc: list nat)
      (action_indices_starting_at_pc_index: array_t (list nat))
      (pc_indices_array: array_t statement_pc_indices_t)
    : GTot bool
val armada_actions_starting_at_pc_correct
      (action_indices_starting_at_no_pc: list nat)
      (action_indices_starting_at_pc_index: array_t (list nat))
      (pc_indices_array: array_t statement_pc_indices_t)
    : GTot bool
let armada_actions_starting_at_pc_correct
  (action_indices_starting_at_no_pc: list nat)
  (action_indices_starting_at_pc_index: array_t (list nat))
  (pc_indices_array: array_t statement_pc_indices_t)
  : GTot bool =
  for_all_array_enumerated
    (armada_actions_starting_at_pc_correct_specific action_indices_starting_at_no_pc
      action_indices_starting_at_pc_index)
    pc_indices_array
module Strategies.RegularToAtomic.Armada

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.Statement
open Armada.Thread
open Armada.Type
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Map
open Spec.Ubool
open Strategies.Atomic
open Strategies.PCIndices
open Strategies.RegularToAtomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.List
open Util.Nth
open Util.Range

type armada_successor_info_t = {
  action_index: nat;
  path_index: nat;
}

type armada_atomic_path_info_t = {
  path: list nat;
  atomic_action_index_or_successors: either nat (list armada_successor_info_t);
}

let armada_is_breaking_optional_pc
  (pc_index_breaking: array_t bool)
  (optional_pc_index: option nat)
  : GTot bool =
  match optional_pc_index with
  | Some pc_index -> if pc_index < array_len pc_index_breaking then array_index pc_index_breaking pc_index else true
  | None -> true

let armada_pc_breaking_correct_specific
  (pc_index_breaking: array_t bool)
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
  let ps = action.program_statement in
     armada_is_breaking_optional_pc pc_index_breaking pc_indices.start_pc_index = ps.starts_atomic_block
  && armada_is_breaking_optional_pc pc_index_breaking pc_indices.end_pc_index = ps.ends_atomic_block
  && (implies (None? ps.end_pc) (armada_is_breaking_optional_pc pc_index_breaking pc_indices.start_pc_index))

let armada_pc_breaking_correct
  (actions_array: array_t Armada.Action.t)
  (pc_indices_array: array_t statement_pc_indices_t)
  (pc_index_breaking: array_t bool)
  : GTot bool =
  arrays_correspond (armada_pc_breaking_correct_specific pc_index_breaking) actions_array pc_indices_array

let armada_created_threads_initially_breaking_specific
  (pc_index_breaking: array_t bool)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
  armada_is_breaking_optional_pc pc_index_breaking pc_indices.create_thread_initial_pc_index

let armada_created_threads_initially_breaking
  (pc_index_breaking: array_t bool)
  (pc_indices_array: array_t statement_pc_indices_t)
  : GTot bool =
  for_all_array (armada_created_threads_initially_breaking_specific pc_index_breaking) pc_indices_array

let armada_actions_starting_at_pc_correct_specific
  (action_indices_starting_at_no_pc: list nat)
  (action_indices_starting_at_pc_index: array_t (list nat))
  (action_index: nat)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
  match pc_indices.start_pc_index with
  | None -> list_contains action_index action_indices_starting_at_no_pc
  | Some pc_index ->
         pc_index < array_len action_indices_starting_at_pc_index
      && list_contains action_index (array_index action_indices_starting_at_pc_index pc_index)
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.fsti.checked Strategies.PCIndices.fst.checked Strategies.Atomic.fst.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.Thread.fst.checked Armada.Statement.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.RegularToAtomic.Armada.fsti

    action_indices_starting_at_no_pc: Prims.list Prims.nat ->
    action_indices_starting_at_pc_index: Util.ImmutableArray.array_t (Prims.list Prims.nat) ->
    pc_indices_array: Util.ImmutableArray.array_t Strategies.PCIndices.statement_pc_indices_t
  -> Prims.GTot Prims.bool
Prims.list Prims.nat Util.ImmutableArray.array_t Strategies.PCIndices.statement_pc_indices_t Util.ImmutableArray.for_all_array_enumerated Strategies.RegularToAtomic.Armada.armada_actions_starting_at_pc_correct_specific Prims.bool
let armada_actions_starting_at_pc_correct
      (action_indices_starting_at_no_pc: list nat)
      (action_indices_starting_at_pc_index: array_t (list nat))
      (pc_indices_array: array_t statement_pc_indices_t)
    : GTot bool =
  
for_all_array_enumerated (armada_actions_starting_at_pc_correct_specific action_indices_starting_at_no_pc
      action_indices_starting_at_pc_index)
  pc_indices_array