val armada_pc_breaking_correct_specific
      (pc_index_breaking: array_t bool)
      (action: Armada.Action.t)
      (pc_indices: statement_pc_indices_t)
    : GTot bool
val armada_pc_breaking_correct_specific
      (pc_index_breaking: array_t bool)
      (action: Armada.Action.t)
      (pc_indices: statement_pc_indices_t)
    : GTot bool
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))
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
/
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

    pc_index_breaking: Util.ImmutableArray.array_t Prims.bool ->
    action: Armada.Action.t ->
    pc_indices: Strategies.PCIndices.statement_pc_indices_t
  -> Prims.GTot Prims.bool
Util.ImmutableArray.array_t Prims.bool Armada.Action.t Strategies.PCIndices.statement_pc_indices_t Prims.op_AmpAmp Prims.op_Equality Strategies.RegularToAtomic.Armada.armada_is_breaking_optional_pc Strategies.PCIndices.__proj__Mkstatement_pc_indices_t__item__start_pc_index Armada.Action.__proj__Mkprogram_statement_t__item__starts_atomic_block Strategies.PCIndices.__proj__Mkstatement_pc_indices_t__item__end_pc_index Armada.Action.__proj__Mkprogram_statement_t__item__ends_atomic_block Spec.Logic.implies FStar.Pervasives.Native.uu___is_None Armada.Base.pc_t Armada.Action.__proj__Mkprogram_statement_t__item__end_pc Armada.Action.program_statement_t Armada.Action.__proj__Mkt__item__program_statement
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))