val pc_breaking_correct_specific (pc_breaking: (pc_t -> GTot bool)) (ps: program_statement_t)
    : GTot bool
val pc_breaking_correct_specific (pc_breaking: (pc_t -> GTot bool)) (ps: program_statement_t)
    : GTot bool
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))
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
/
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
pc_breaking: (_: Armada.Base.pc_t -> Prims.GTot Prims.bool) -> ps: Armada.Action.program_statement_t
  -> Prims.GTot Prims.bool
Armada.Base.pc_t Prims.bool Armada.Action.program_statement_t Prims.op_AmpAmp Prims.op_Equality Strategies.RegularToAtomic.Armada.Helper.is_breaking_optional_pc Armada.Action.__proj__Mkprogram_statement_t__item__start_pc Armada.Action.__proj__Mkprogram_statement_t__item__starts_atomic_block Armada.Action.__proj__Mkprogram_statement_t__item__end_pc Armada.Action.__proj__Mkprogram_statement_t__item__ends_atomic_block Spec.Logic.implies FStar.Pervasives.Native.uu___is_None
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))