val all_threads_breaking (ra: regular_refines_atomic_relation_t) (s: ra.sem.state_t) : GTot ubool
val all_threads_breaking (ra: regular_refines_atomic_relation_t) (s: ra.sem.state_t) : GTot ubool
let all_threads_breaking
  (ra: regular_refines_atomic_relation_t)
  (s: ra.sem.state_t)
  : GTot ubool =
  forall actor. ra.is_breaking_state s actor
module Strategies.RegularToAtomic

open Armada.Action
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Transition
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.Atomic
open Strategies.Semantics
open Util.Behavior
open Util.List
open Util.Logic
open Util.Nth
/
Util.Nth.fst.checked Util.Logic.fst.checked Util.List.fst.checked Util.Behavior.fst.checked Strategies.Semantics.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.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 FStar.Classical.Sugar.fsti.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Action.fst.checked
Strategies.RegularToAtomic.fst

    ra: Strategies.RegularToAtomic.regular_refines_atomic_relation_t ->
    s: Mksemantics_t?.state_t (Mkregular_refines_atomic_relation_t?.sem ra)
  -> Prims.GTot Spec.Ubool.ubool
Strategies.RegularToAtomic.regular_refines_atomic_relation_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.RegularToAtomic.__proj__Mkregular_refines_atomic_relation_t__item__sem Prims.l_Forall Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Prims.b2t Strategies.RegularToAtomic.__proj__Mkregular_refines_atomic_relation_t__item__is_breaking_state Spec.Ubool.ubool
let all_threads_breaking (ra: regular_refines_atomic_relation_t) (s: ra.sem.state_t) : GTot ubool =
  
forall actor. ra.is_breaking_state s actor