val armada_atomic_substep_special_cases_apply : inv: Strategies.Invariant.invariant_t Armada.State.t ->
    action_pred: (_: Armada.Action.t -> Prims.GTot Spec.Ubool.ubool) ->
    program_actions: Prims.list (Prims.list Armada.Action.t) ->
    special_case_proofs:
      Prims.list (Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Armada.armada_action_special_case_invariant_proof_t
                    inv)))
  -> Spec.Ubool.ubool
let armada_atomic_substep_special_cases_apply
  (inv: invariant_t Armada.State.t)
  (action_pred: Armada.Action.t -> GTot ubool)
  (program_actions: list (list Armada.Action.t))
  (special_case_proofs: (list (list (option (armada_action_special_case_invariant_proof_t inv))))) =
  lists_correspond_ubool
    (lists_correspond_ubool (armada_action_proof_option_applies inv action_pred))
    program_actions
    special_case_proofs
module Strategies.Invariant.Armada.AtomicSubstep

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.Semantics
open Strategies.Semantics.Armada
open Strategies.Invariant
open Strategies.Invariant.Armada
open Util.List

noeq type armada_atomic_substep_invariant_witness_t
  (program: program_t (make_atomic_semantics armada_semantics))
  (inv: invariant_t Armada.State.t) =
{
  action_pred: Armada.Action.t -> GTot ubool;
  special_case_proofs: list (list (option (armada_action_special_case_invariant_proof_t inv)));
  init_implies_inv_proof: (s: Armada.State.t{program.init_f s}) -> squash (inv s);
  action_proof: armada_action_maintains_invariant_proof_t inv action_pred;
}
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.fsti.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.AtomicSubstep.fsti

    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    action_pred: (_: Armada.Action.t -> Prims.GTot Spec.Ubool.ubool) ->
    program_actions: Prims.list (Prims.list Armada.Action.t) ->
    special_case_proofs:
      Prims.list (Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Armada.armada_action_special_case_invariant_proof_t
                    inv)))
  -> Spec.Ubool.ubool
Strategies.Invariant.invariant_t Armada.State.t Armada.Action.t Spec.Ubool.ubool Prims.list FStar.Pervasives.Native.option Strategies.Invariant.Armada.armada_action_special_case_invariant_proof_t Util.List.lists_correspond_ubool Strategies.Invariant.Armada.armada_action_proof_option_applies
let armada_atomic_substep_special_cases_apply
      (inv: invariant_t Armada.State.t)
      (action_pred: (Armada.Action.t -> GTot ubool))
      (program_actions: list (list Armada.Action.t))
      (special_case_proofs:
          (list (list (option (armada_action_special_case_invariant_proof_t inv)))))
     =
  
lists_correspond_ubool (lists_correspond_ubool (armada_action_proof_option_applies inv action_pred))
  program_actions
  special_case_proofs