val is_breaking_optional_pc (pc_breaking: (pc_t -> GTot bool)) (optional_pc: option pc_t)
    : GTot bool
val is_breaking_optional_pc (pc_breaking: (pc_t -> GTot bool)) (optional_pc: option pc_t)
    : GTot bool
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
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
/
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) ->
    optional_pc: FStar.Pervasives.Native.option Armada.Base.pc_t
  -> Prims.GTot Prims.bool
Armada.Base.pc_t Prims.bool FStar.Pervasives.Native.option
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