val 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
val 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
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
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))
/
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

    actions_array: Util.ImmutableArray.array_t Armada.Action.t ->
    pc_indices_array: Util.ImmutableArray.array_t Strategies.PCIndices.statement_pc_indices_t ->
    pc_index_breaking: Util.ImmutableArray.array_t Prims.bool
  -> Prims.GTot Prims.bool
Util.ImmutableArray.array_t Armada.Action.t Strategies.PCIndices.statement_pc_indices_t Prims.bool Util.ImmutableArray.arrays_correspond Strategies.RegularToAtomic.Armada.armada_pc_breaking_correct_specific
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