val is_inductive_armada_invariant_of_program
      (inv: invariant_t Armada.State.t)
      (program: Armada.Program.t)
    : GTot ubool
val is_inductive_armada_invariant_of_program
      (inv: invariant_t Armada.State.t)
      (program: Armada.Program.t)
    : GTot ubool
let is_inductive_armada_invariant_of_program
  (inv: invariant_t Armada.State.t)
  (program: Armada.Program.t)
  : GTot ubool
  =   (forall (s: Armada.State.t). init_program program s ==> inv s)
    /\ (forall (s s': Armada.State.t) (transition: Armada.Transition.t).
          inv s /\ next_program program transition s s' ==> inv s')
module Strategies.Invariant.Armada

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Transition
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.List
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.fsti.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 Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.Invariant.Armada.fsti
inv: Strategies.Invariant.invariant_t Armada.State.t -> program: Armada.Program.t
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Invariant.invariant_t Armada.State.t Armada.Program.t Prims.l_and Prims.l_Forall Prims.l_imp Armada.Program.init_program Armada.Transition.t Armada.Program.next_program Spec.Ubool.ubool
let is_inductive_armada_invariant_of_program
      (inv: invariant_t Armada.State.t)
      (program: Armada.Program.t)
    : GTot ubool =
  
(forall (s: Armada.State.t). init_program program s ==> inv s) /\
(forall (s: Armada.State.t) (s': Armada.State.t) (transition: Armada.Transition.t).
    inv s /\ next_program program transition s s' ==> inv s')