val all_threads_breaking_except
      (ra: regular_refines_atomic_relation_t)
      (s: ra.sem.state_t)
      (actor: ra.sem.actor_t)
    : GTot ubool
val all_threads_breaking_except
      (ra: regular_refines_atomic_relation_t)
      (s: ra.sem.state_t)
      (actor: ra.sem.actor_t)
    : GTot ubool
let all_threads_breaking_except
  (ra: regular_refines_atomic_relation_t)
  (s: ra.sem.state_t)
  (actor: ra.sem.actor_t)
  : GTot ubool =
  forall other_actor. actor <> other_actor ==> ra.is_breaking_state s other_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

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
/
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) ->
    actor: Mksemantics_t?.actor_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 Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Prims.l_Forall Prims.l_imp Prims.b2t Prims.op_disEquality Strategies.RegularToAtomic.__proj__Mkregular_refines_atomic_relation_t__item__is_breaking_state Spec.Ubool.ubool
let all_threads_breaking_except
      (ra: regular_refines_atomic_relation_t)
      (s: ra.sem.state_t)
      (actor: ra.sem.actor_t)
    : GTot ubool =
  
forall other_actor. actor <> other_actor ==> ra.is_breaking_state s other_actor