val behavior_refines_behavior
      (#low_state_t #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
val behavior_refines_behavior
      (#low_state_t #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
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)
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 }
/
Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Spec.Behavior.fst

    lb: Spec.Behavior.behavior_t low_state_t ->
    hb: Spec.Behavior.behavior_t high_state_t ->
    rr: Spec.Behavior.refinement_relation_t low_state_t high_state_t
  -> Prims.GTot Spec.Ubool.ubool
Spec.Behavior.behavior_t Spec.Behavior.refinement_relation_t Prims.b2t Prims.uu___is_Nil Prims.list Prims.l_and Prims.l_or Spec.Behavior.behavior_refines_behavior Spec.Ubool.ubool
let rec behavior_refines_behavior
      (#low_state_t #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 \/ behavior_refines_behavior ltail hb rr \/
      behavior_refines_behavior lb htail rr)