val is_inductive_invariant_of_spec
      (#state_t: Type)
      (inv: invariant_t state_t)
      (spec: spec_t state_t)
    : GTot ubool
val is_inductive_invariant_of_spec
      (#state_t: Type)
      (inv: invariant_t state_t)
      (spec: spec_t state_t)
    : GTot ubool
let is_inductive_invariant_of_spec
  (#state_t: Type)
  (inv: invariant_t state_t)
  (spec: spec_t state_t)
  : GTot ubool
  =   (forall (s: state_t). spec.init s ==> inv s)
    /\ (forall (s s': state_t). inv s /\ (spec.next s s') ==> inv s')
module Strategies.Invariant

open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.Semantics
open Util.List

/// Proving invariants of arbitrary state machines

type invariant_t (state_t: Type) = state_t -> GTot ubool

let is_invariant_of_behavior
  (#state_t: Type)
  (inv: invariant_t state_t)
  (b: behavior_t state_t)
  : GTot ubool
  = forall s. contains_ubool s b ==> inv s

let is_invariant_of_spec
  (#state_t: Type)
  (inv: invariant_t state_t)
  (spec: spec_t state_t)
  : GTot ubool
  = forall (b: behavior_t state_t). behavior_satisfies_spec b spec ==> is_invariant_of_behavior inv b
/
Util.List.fst.checked Strategies.Semantics.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Strategies.Invariant.fsti
inv: Strategies.Invariant.invariant_t state_t -> spec: Spec.Behavior.spec_t state_t
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Invariant.invariant_t Spec.Behavior.spec_t Prims.l_and Prims.l_Forall Prims.l_imp Spec.Behavior.__proj__Mkspec_t__item__init Spec.Behavior.__proj__Mkspec_t__item__next Spec.Ubool.ubool
let is_inductive_invariant_of_spec
      (#state_t: Type)
      (inv: invariant_t state_t)
      (spec: spec_t state_t)
    : GTot ubool =
  
(forall (s: state_t). spec.init s ==> inv s) /\
(forall (s: state_t) (s': state_t). inv s /\ (spec.next s s') ==> inv s')