val actor_memory_predicate_transitive : pred: Strategies.ArmadaStatement.actor_memory_predicate -> Prims.logical
let actor_memory_predicate_transitive (pred: actor_memory_predicate) =
  forall actor x1 x2 x3. (pred actor x1 x2 /\ pred actor x2 x3) ==> (pred actor x1 x3)
module Strategies.ArmadaStatement

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open Spec.List
open Spec.Logic
open Spec.Ubool
open Util.List

let actor_state_predicate = tid_t -> Armada.State.t -> Armada.State.t -> Type0

let actor_state_predicate_transitive (pred: actor_state_predicate) =
  forall actor x1 x2 x3. (pred actor x1 x2 /\ pred actor x2 x3) ==> (pred actor x1 x3)

let actor_state_predicate_reflexive (pred: actor_state_predicate) =
  forall actor x. pred actor x x

let actor_memory_predicate = tid_t -> Armada.Memory.t -> Armada.Memory.t -> Type0
/
Util.List.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.ArmadaStatement.fst
pred: Strategies.ArmadaStatement.actor_memory_predicate -> Prims.logical
Strategies.ArmadaStatement.actor_memory_predicate Prims.l_Forall Armada.Base.tid_t Armada.Memory.t Prims.l_imp Prims.l_and Prims.logical
let actor_memory_predicate_transitive (pred: actor_memory_predicate) =
  
forall actor x1 x2 x3. (pred actor x1 x2 /\ pred actor x2 x3) ==> (pred actor x1 x3)