val refinement_requirement (ls hs: Armada.State.t) : GTot ubool
val refinement_requirement (ls hs: Armada.State.t) : GTot ubool
let refinement_requirement (ls: Armada.State.t) (hs: Armada.State.t) : GTot ubool =
  if NotStopped? ls.stop_reason then
    is_prefix ls.trace hs.trace
  else
    ls.stop_reason = hs.stop_reason /\ ls.trace == hs.trace
module Armada.State

open Armada.Base
open Armada.Memory
open Armada.Threads
open Armada.Type
open FStar.Sequence.Base
open Spec.Behavior
open Spec.List
open Spec.Ubool

type stop_reason_t =
  | NotStopped
  | StopReasonTerminated
  | StopReasonAssertionFailure
  | StopReasonUndefinedBehavior
  | StopReasonStackOverflow

type trace_entry = object_value_t

noeq type t = {
  initial_tid: tid_t;
  uniqs_used: list root_id_uniquifier_t;
  mem: Armada.Memory.t;
  threads: Armada.Threads.t;
  trace: seq trace_entry;
  stop_reason: stop_reason_t;
}
/
Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Memory.fst.checked Armada.Base.fst.checked
Armada.State.fst
ls: Armada.State.t -> hs: Armada.State.t -> Prims.GTot Spec.Ubool.ubool
Armada.State.t Armada.State.uu___is_NotStopped Armada.State.__proj__Mkt__item__stop_reason FStar.Sequence.Base.is_prefix Armada.State.trace_entry Armada.State.__proj__Mkt__item__trace Prims.bool Prims.l_and Prims.b2t Prims.op_Equality Armada.State.stop_reason_t Prims.eq2 FStar.Sequence.Base.seq Spec.Ubool.ubool
let refinement_requirement (ls hs: Armada.State.t) : GTot ubool =
  
if NotStopped? ls.stop_reason
then is_prefix ls.trace hs.trace
else ls.stop_reason = hs.stop_reason /\ ls.trace == hs.trace