val next_transition (transition: Armada.Transition.t) (s s': Armada.State.t) : GTot bool
val next_transition (transition: Armada.Transition.t) (s s': Armada.State.t) : GTot bool
let next_transition (transition: Armada.Transition.t) (s s': Armada.State.t) : GTot bool =
  eqb (Some s') (steps_computation transition.actor true true transition.steps s)
module Armada.Transition

open Armada.Action
open Armada.Base
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Threads
open Armada.Type
open Spec.List
open Spec.Ubool

noeq type t = {
  actor: tid_t;
  steps: list Armada.Step.t;
}

let step_computation
  (actor: tid_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (step: Armada.Step.t)
  (s: Armada.State.t)
  : GTot (option Armada.State.t) =
  action_computation actor starts_atomic_block ends_atomic_block step.nd step.action s

let rec steps_computation
  (actor: tid_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (steps: list Armada.Step.t)
  (s: Armada.State.t)
  : GTot (option Armada.State.t)
    (decreases steps) =
  match steps with
  | [] -> None
  | [last_step] -> step_computation actor starts_atomic_block ends_atomic_block last_step s
  | first_step :: remaining_steps ->
      (match step_computation actor starts_atomic_block false first_step s with
       | None -> None
       | Some s' -> steps_computation actor false ends_atomic_block remaining_steps s')
/
Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Armada.Transition.fst
transition: Armada.Transition.t -> s: Armada.State.t -> s': Armada.State.t -> Prims.GTot Prims.bool
Armada.Transition.t Armada.State.t Spec.Ubool.eqb FStar.Pervasives.Native.option FStar.Pervasives.Native.Some Armada.Transition.steps_computation Armada.Transition.__proj__Mkt__item__actor Armada.Transition.__proj__Mkt__item__steps Prims.bool
let next_transition (transition: Armada.Transition.t) (s s': Armada.State.t) : GTot bool =
  
eqb (Some s') (steps_computation transition.actor true true transition.steps s)