val behavior_satisfies_next
      (#state_t: Type)
      (b: behavior_t state_t)
      (next: (state_t -> state_t -> GTot ubool))
    : GTot ubool
val behavior_satisfies_next
      (#state_t: Type)
      (b: behavior_t state_t)
      (next: (state_t -> state_t -> GTot ubool))
    : GTot ubool
let rec behavior_satisfies_next
  (#state_t: Type)
  (b: behavior_t state_t)
  (next: state_t -> state_t -> GTot ubool)
  : GTot ubool =
  match b with
  | [] -> True
  | [s] -> True
  | s1 :: s2 :: tl -> next s1 s2 /\ behavior_satisfies_next (s2 :: tl) next
module Spec.Behavior

open Spec.Ubool

type behavior_t (a: Type) = list a
type refinement_relation_t (low_state_t high_state_t: Type) = low_state_t -> high_state_t -> GTot ubool
noeq type spec_t (state_t: Type) = { init: state_t -> GTot ubool; next: state_t -> state_t -> GTot ubool }

let rec behavior_refines_behavior
  (#low_state_t: Type)
  (#high_state_t: Type)
  (lb: behavior_t low_state_t)
  (hb: behavior_t high_state_t)
  (rr: refinement_relation_t low_state_t high_state_t)
  : GTot ubool =
  match lb with
  | [] -> Nil? hb
  | lstate :: ltail ->
    match hb with
    | [] -> false
    | hstate :: htail ->
      rr lstate hstate /\
      (  behavior_refines_behavior ltail htail rr // neither behavior stutters at the beginning
       \/ behavior_refines_behavior ltail hb rr  // behavior #1 stutters at the beginning
       \/ behavior_refines_behavior lb htail rr) // behavior #2 stutters at the beginning
/
Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Spec.Behavior.fst

    b: Spec.Behavior.behavior_t state_t ->
    next: (_: state_t -> _: state_t -> Prims.GTot Spec.Ubool.ubool)
  -> Prims.GTot Spec.Ubool.ubool
Spec.Behavior.behavior_t Spec.Ubool.ubool Prims.l_True Prims.list Prims.l_and Spec.Behavior.behavior_satisfies_next Prims.Cons
let rec behavior_satisfies_next
      (#state_t: Type)
      (b: behavior_t state_t)
      (next: (state_t -> state_t -> GTot ubool))
    : GTot ubool =
  
match b with
| [] -> True
| [s] -> True
| s1 :: s2 :: tl -> next s1 s2 /\ behavior_satisfies_next (s2 :: tl) next